Documentation

Mathlib.AlgebraicGeometry.Fiber

Scheme-theoretic fiber #

Main result #

source
def AlgebraicGeometry.Scheme.Hom.fiber {X Y : Scheme} (f : X ⟶ 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 ⟶ Y) (y : ↥Y) :
      fiber f 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 ⟶ Y) (y : ↥Y) :
          (Scheme.Hom.fiber f y).CanonicallyOver X
          Equations
            source
            def AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) :
            fiber f 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 ⟶ Y) (y : ↥Y) :
                (fiber f 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 ⟶ Y) (y : ↥Y) (x : ↥(fiber f y)) :
                    (fiberToSpecResidueField f y) x = IsLocalRing.closedPoint ↑(Y.residueField y)
                    source
                    theorem AlgebraicGeometry.Scheme.Hom.range_fiberι {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) :
                    Set.range ⇑(fiberι f y) = ⇑f ⁻¹' {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 ⟶ Y) (y : ↥Y) :
                    ↥(fiber f y) ≃ₜ ↑(⇑f ⁻¹' {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 ⟶ Y) (y : ↥Y) (x : ↥(fiber f y)) :
                        ↑((fiberHomeo f y) x) = (fiberι f y) x
                        source
                        @[simp]
                        theorem AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) (x : ↑(⇑f ⁻¹' {y})) :
                        (fiberι f y) ((fiberHomeo f y).symm x) = ↑x
                        source
                        def AlgebraicGeometry.Scheme.Hom.asFiber {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) :
                        ↥(fiber f (f 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 ⟶ Y) (x : ↥X) :
                            (fiberι f (f x)) (asFiber f 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.Scheme.Hom.isCompact_preimage_singleton {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (y : ↥Y) :
                            IsCompact (⇑f ⁻¹' {y})
                            source
                            @[deprecated AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton (since := "2026-02-05")]
                            theorem AlgebraicGeometry.QuasiCompact.isCompact_preimage_singleton {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (y : ↥Y) :
                            IsCompact (⇑f ⁻¹' {y})

                            Alias of AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton.

                            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
                            def AlgebraicGeometry.Scheme.Hom.asFiberHom {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) :
                            Spec (X.residueField x) ⟶ fiber f (f x)

                            The κ(x)-point of f ⁻¹' {f x} corresponding to x.

                            Equations
                              Instances For
                                source
                                @[simp]
                                theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) :
                                CategoryTheory.CategoryStruct.comp (asFiberHom f x) (fiberι f (f x)) = X.fromSpecResidueField x
                                source
                                @[simp]
                                theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι_assoc {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) {Z : Scheme} (h : X ⟶ Z) :
                                CategoryTheory.CategoryStruct.comp (asFiberHom f x) (CategoryTheory.CategoryStruct.comp (fiberι f (f x)) h) = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) h
                                source
                                @[simp]
                                theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) :
                                CategoryTheory.CategoryStruct.comp (asFiberHom f x) (fiberToSpecResidueField f (f x)) = Spec.map (residueFieldMap f x)
                                source
                                @[simp]
                                theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField_assoc {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) {Z : Scheme} (h : Spec (Y.residueField (f x)) ⟶ Z) :
                                CategoryTheory.CategoryStruct.comp (asFiberHom f x) (CategoryTheory.CategoryStruct.comp (fiberToSpecResidueField f (f x)) h) = CategoryTheory.CategoryStruct.comp (Spec.map (residueFieldMap f x)) h
                                source
                                @[simp]
                                theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_apply {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) (y : ↥(Spec (X.residueField x))) :
                                (asFiberHom f x) y = asFiber f x
                                source
                                @[simp]
                                theorem AlgebraicGeometry.Scheme.Hom.range_asFiberHom {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) :
                                Set.range ⇑(asFiberHom f x) = {asFiber f x}
                                source
                                instance AlgebraicGeometry.instIsPreimmersionAsFiberHom {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) :
                                IsPreimmersion (Scheme.Hom.asFiberHom f x)