Module

ProperClosedFiberFaithful.lean

Nyll.SchemeTheory.FiniteEtale.ProperClosedFiberFaithful

2 declarations indexed from sourceView source ↗

Module documentation

Faithful finite étale pullback to a proper closed fibre

Over any local ring, finite étale morphisms on a proper scheme are determined by their restriction to the closed fibre. The proof uses the actual relative equalizer, which is open and closed, and the existing proper closed-fibre isomorphism detector. Neither Noetherianity nor henselianity is assumed.

Imports6

Nyll.SchemeTheory.FiniteEtale.isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Nyll.SchemeTheory.Morphisms.UnramifiedHomExt
Mathlib.AlgebraicGeometry.Morphisms.Proper
Mathlib.CategoryTheory.EpiMono
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Imported by2

theorem

hom_ext_of_closedFiber_of_isProper

L33 ↗

AlgebraicGeometry.Over.hom_ext_of_closedFiber_of_isProper

Documentation

Relative maps into a separated unramified scheme are determined by the closed fibre when their source is proper over a local ring.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry

Lean source · statement

theorem Over.hom_ext_of_closedFiber_of_isProper
    {R : Type u} [CommRing R] [IsLocalRing R]
    {S : Scheme.{u}} {U V : Over S}
    (f : U.left ⟶ AlgebraicGeometry.Spec (CommRingCat.of R)) [IsProper f]
    [FormallyUnramified V.hom] [LocallyOfFiniteType V.hom] [IsSeparated V.hom]
    (a b : U ⟶ V)
    (h : pullback.fst f
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))) ≫ a.left =
      pullback.fst f
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))) ≫ b.left) :
    a = b

theorem

pullback_faithful_closedFiber_of_isProper

L78 ↗

AlgebraicGeometry.FiniteEtale.pullback_faithful_closedFiber_of_isProper

Documentation

Pullback to the closed fibre of a proper scheme over any local ring is faithful on finite étale schemes. No henselian or Noetherian hypothesis is needed.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
namespace FiniteEtale

Lean source · full declaration

theorem pullback_faithful_closedFiber_of_isProper
    {R : Type u} [CommRing R] [IsLocalRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f] :
    (FiniteEtale.pullback
      (pullback.fst f (Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))))).Faithful where
  map_injective {A B} a b hab := by
    let r := Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))
    let i := pullback.fst f r
    have hleft : ((FiniteEtale.pullback i).map a).left =
        ((FiniteEtale.pullback i).map b).left :=
      congrArg (fun q : (FiniteEtale.pullback i).obj A ⟶
        (FiniteEtale.pullback i).obj B ↦ q.left) hab
    have hcomp : pullback.fst A.hom i ≫ a.left =
        pullback.fst A.hom i ≫ b.left := by
      have ha : pullback.fst A.hom i ≫ a.left =
          ((FiniteEtale.pullback i).map a).left ≫ pullback.fst B.hom i :=
        (pullback.lift_fst _ _ _).symm
      have hb : ((FiniteEtale.pullback i).map b).left ≫ pullback.fst B.hom i =
          pullback.fst A.hom i ≫ b.left := pullback.lift_fst _ _ _
      exact ha.trans ((congrArg (fun k ↦ k ≫ pullback.fst B.hom i) hleft).trans hb)
    have hclosed : pullback.fst (A.hom ≫ f) r ≫ a.left =
        pullback.fst (A.hom ≫ f) r ≫ b.left := by
      rw [← pullbackRightPullbackFstIso_inv_fst f r A.hom]
      simp only [Category.assoc]
      exact congrArg ((pullbackRightPullbackFstIso f r A.hom).inv ≫ ·) hcomp
    have hOver : a.hom = b.hom :=
      AlgebraicGeometry.Over.hom_ext_of_closedFiber_of_isProper
        (A.hom ≫ f) a.hom b.hom hclosed
    apply MorphismProperty.Over.Hom.ext
    exact congrArg (fun q : A.toComma ⟶ B.toComma ↦ q.left) hOver

Module documentation

Faithful finite étale pullback to a proper closed fibre

Declarations

hom_ext_of_closedFiber_of_isProper

pullback_faithful_closedFiber_of_isProper