Documentation

Mathlib.AlgebraicGeometry.Fiber

Scheme-theoretic fiber #

Main result #

source
def AlgebraicGeometry.Scheme.Hom.fiber {X Y : Scheme} (f : X.Hom Y) (y : ↥Y) :
Scheme

f.fiber y is the scheme theoretic fiber of f at y.

Equations
    Instances For
      source
      def AlgebraicGeometry.Scheme.Hom.fiberι {X Y : Scheme} (f : X.Hom Y) (y : ↥Y) :
      f.fiber y ⟶ X

      f.fiberι y : f.fiber y ⟶ X is the embedding of the scheme theoretic fiber into X.

      Equations
        Instances For
          source
          instance AlgebraicGeometry.instCanonicallyOverFiber {X Y : Scheme} (f : X.Hom Y) (y : ↥Y) :
          (f.fiber y).CanonicallyOver X
          Equations
            source
            def AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField {X Y : Scheme} (f : X.Hom Y) (y : ↥Y) :
            f.fiber y ⟶ Spec (Y.residueField y)

            The canonical map from the scheme theoretic fiber to the residue field.

            Equations
              Instances For
                source
                @[reducible]
                def AlgebraicGeometry.Scheme.Hom.fiberOverSpecResidueField {X Y : Scheme} (f : X.Hom Y) (y : ↥Y) :
                (f.fiber y).Over (Spec (Y.residueField y))

                The fiber of f at y is naturally a κ(y)-scheme.

                Equations
                  Instances For
                    source
                    theorem AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField_apply {X Y : Scheme} (f : X.Hom Y) (y : ↥Y) (x : ↥(f.fiber y)) :
                    (CategoryTheory.ConcreteCategory.hom (f.fiberToSpecResidueField y).base) x = IsLocalRing.closedPoint ↑(Y.residueField y)
                    source
                    theorem AlgebraicGeometry.Scheme.Hom.range_fiberι {X Y : Scheme} (f : X.Hom Y) (y : ↥Y) :
                    Set.range ⇑(CategoryTheory.ConcreteCategory.hom (f.fiberι y).base) = ⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' {y}
                    source
                    instance AlgebraicGeometry.instIsPreimmersionFiberι {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) :
                    IsPreimmersion (Scheme.Hom.fiberι f y)
                    source
                    def AlgebraicGeometry.Scheme.Hom.fiberHomeo {X Y : Scheme} (f : X.Hom Y) (y : ↥Y) :
                    ↥(f.fiber y) ≃ₜ ↑(⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' {y})

                    The scheme theoretic fiber of f at y is homeomorphic to f ⁻¹' {y}.

                    Equations
                      Instances For
                        source
                        @[simp]
                        theorem AlgebraicGeometry.Scheme.Hom.fiberHomeo_apply {X Y : Scheme} (f : X.Hom Y) (y : ↥Y) (x : ↥(f.fiber y)) :
                        ↑((f.fiberHomeo y) x) = (CategoryTheory.ConcreteCategory.hom (f.fiberι y).base) x
                        source
                        @[simp]
                        theorem AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm {X Y : Scheme} (f : X.Hom Y) (y : ↥Y) (x : ↑(⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' {y})) :
                        (CategoryTheory.ConcreteCategory.hom (f.fiberι y).base) ((f.fiberHomeo y).symm x) = ↑x
                        source
                        def AlgebraicGeometry.Scheme.Hom.asFiber {X Y : Scheme} (f : X.Hom Y) (x : ↥X) :
                        ↥(f.fiber ((CategoryTheory.ConcreteCategory.hom f.base) x))

                        A point x as a point in the fiber of f at f x.

                        Equations
                          Instances For
                            source
                            @[simp]
                            theorem AlgebraicGeometry.Scheme.Hom.fiberι_asFiber {X Y : Scheme} (f : X.Hom Y) (x : ↥X) :
                            (CategoryTheory.ConcreteCategory.hom (f.fiberι ((CategoryTheory.ConcreteCategory.hom f.base) x)).base) (f.asFiber x) = x
                            source
                            instance AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (y : ↥Y) :
                            CompactSpace ↥(Scheme.Hom.fiber f y)
                            source
                            theorem AlgebraicGeometry.QuasiCompact.isCompact_preimage_singleton {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (y : ↥Y) :
                            IsCompact (⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' {y})
                            source
                            instance AlgebraicGeometry.instIsAffineFiberOfIsAffineHom {X Y : Scheme} (f : X ⟶ Y) [IsAffineHom f] (y : ↥Y) :
                            IsAffine (Scheme.Hom.fiber f y)
                            source
                            instance AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) [LocallyOfFiniteType f] :
                            JacobsonSpace ↥(Scheme.Hom.fiber f y)
                            source
                            instance AlgebraicGeometry.instFiniteCarrierCarrierCommRingCatFiberOfIsFinite {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) [IsFinite f] :
                            Finite ↥(Scheme.Hom.fiber f y)
                            source
                            theorem AlgebraicGeometry.IsFinite.finite_preimage_singleton {X Y : Scheme} (f : X ⟶ Y) [IsFinite f] (y : ↥Y) :
                            (⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' {y}).Finite
                            source
                            theorem AlgebraicGeometry.Scheme.Hom.finite_preimage {X Y : Scheme} (f : X.Hom Y) [IsFinite f] {s : Set ↥Y} (hs : s.Finite) :
                            (⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' s).Finite
                            source
                            instance AlgebraicGeometry.Scheme.Hom.discrete_fiber {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) [IsFinite f] :
                            DiscreteTopology ↥(fiber f y)