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)) :
          (CategoryTheory.ConcreteCategory.hom (fiberToSpecResidueField f y).base) x = IsLocalRing.closedPoint ↑(Y.residueField y)
          source
          theorem AlgebraicGeometry.Scheme.Hom.range_fiberι {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) :
          Set.range ⇑(CategoryTheory.ConcreteCategory.hom (fiberι f 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 ⟶ Y) (y : ↥Y) :
          ↥(fiber f 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 ⟶ Y) (y : ↥Y) (x : ↥(fiber f y)) :
            ↑((fiberHomeo f y) x) = (CategoryTheory.ConcreteCategory.hom (fiberι f y).base) x
            source
            @[simp]
            theorem AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) (x : ↑(⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' {y})) :
            (CategoryTheory.ConcreteCategory.hom (fiberι f y).base) ((fiberHomeo f y).symm x) = ↑x
            source
            def AlgebraicGeometry.Scheme.Hom.asFiber {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) :
            ↥(fiber f ((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 ⟶ Y) (x : ↥X) :
              (CategoryTheory.ConcreteCategory.hom (fiberι f ((CategoryTheory.ConcreteCategory.hom f.base) x)).base) (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.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 ⟶ 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)