Nyll.EtaleFundamentalGroups.Normalization.GlobalFiberDegreeCriterion

instance

fieldSpecQuasiCompact

EtaleFundamentalGroups.fieldSpecQuasiCompact

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

theorem

normalizationChart_fiber_degree

L43 ↗

EtaleFundamentalGroups.normalizationChart_fiber_degree

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

Lean source · full declaration

theorem normalizationChart_fiber_degree
    (X : Scheme.{u}) [IsIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L]
    (U : X.Opens) (hU : IsAffineOpen U) [Nonempty U]
    (p : PrimeSpectrum Γ(X, U)) (n : ℕ)
    (hfiber : Etale ((X.genericExtensionMorphism L).fromNormalization.fiberToSpecResidueField
        (hU.fromSpec p)) ∧
      n ≤ ((X.genericExtensionMorphism L).fromNormalization.fiberToSpecResidueField
        (hU.fromSpec p)).finrank (IsLocalRing.closedPoint (X.residueField (hU.fromSpec p)))) :
    let : Algebra Γ(X, U) L := X.affineExtensionAlgebra U L
    Algebra.Etale p.asIdeal.ResidueField
        (p.asIdeal.ResidueField ⊗[Γ(X, U)] integralClosure Γ(X, U) L) ∧
      n ≤ Module.finrank p.asIdeal.ResidueField
        (p.asIdeal.ResidueField ⊗[Γ(X, U)] integralClosure Γ(X, U) L) := by
  intro actualAlgebra
  let R := Γ(X, U)
  let p₀ : Spec R := p
  let B := integralClosure R L
  let k := p.asIdeal.ResidueField
  let C := k ⊗[R] B
  let f := (X.genericExtensionMorphism L).fromNormalization
  let x := hU.fromSpec p₀
  let b := X.fromSpecResidueField x
  let g := f.fiberToSpecResidueField x
  have hOpen : IsOpenImmersion hU.fromSpec := IsAffineOpen.isOpenImmersion_fromSpec hU
  have hResidue : IsIso (hU.fromSpec.residueFieldMap p₀) :=
    (IsLocalRing.ResidueField.mapEquiv
      (asIso (hU.fromSpec.stalkMap p₀)).commRingCatIsoToRingEquiv).toCommRingCatIso.isIso_hom
  let eSpec := Scheme.Spec.residueFieldIso R p₀
  let e : X.residueField x ≅ CommRingCat.of k :=
    asIso (hU.fromSpec.residueFieldMap p₀) ≪≫ eSpec
  let a := Spec.map e.hom
  let v := Spec.map (CommRingCat.ofHom (algebraMap R k))
  let q := Spec.map (CommRingCat.ofHom (algebraMap k C))
  let d := Spec.map (CommRingCat.ofHom
    (Algebra.TensorProduct.includeRight : B →ₐ[R] C).toRingHom)
  have hSpec : Spec.map eSpec.hom ≫ (Spec R).fromSpecResidueField p₀ = v := by
    rw [← Scheme.Spec.map_residueFieldIso_inv_eq_fromSpecResidueField R p₀,
      ← Category.assoc, ← Spec.map_comp, eSpec.inv_hom_id, Spec.map_id, Category.id_comp]
  have hab : a ≫ b = v ≫ hU.fromSpec := by
    change Spec.map ((hU.fromSpec.residueFieldMap p₀) ≫ eSpec.hom) ≫ b = _
    rw [Spec.map_comp, Category.assoc,
      hU.fromSpec.SpecMap_residueFieldMap_fromSpecResidueField p₀, ← Category.assoc, hSpec]
  have htensor : IsPullback q d v
      (Spec.map (CommRingCat.ofHom (algebraMap R B))) :=
    isPullback_SpecMap_of_isPushout _ _ _ _ (CommRingCat.isPushout_tensorProduct R k B)
  have htotal := htensor.paste_vert (isPullback_genericNormalizationChart X L U hU)
  rw [← hab] at htotal
  have H := (htotal.of_bot' (IsPullback.of_hasPullback f b).flip).flip
  have : Etale g := hfiber.1
  have hIntegral : IsIntegralHom f :=
    inferInstanceAs (IsIntegralHom (X.genericExtensionMorphism L).fromNormalization)
  have : IsIntegralHom g := MorphismProperty.of_isPullback
    (P := (@IsIntegralHom : MorphismProperty Scheme.{u}))
    (IsPullback.of_hasPullback f b) hIntegral
  have : IsFinite g := (IsFinite.iff_isIntegralHom_and_locallyOfFiniteType g).mpr
    ⟨inferInstance, inferInstance⟩
  have : MorphismProperty.IsStableUnderBaseChange
      (@Etale : MorphismProperty Scheme.{u}) :=
    HasRingHomProperty.isStableUnderBaseChange
      (P := (@Etale : MorphismProperty Scheme.{u})) RingHom.Etale.isStableUnderBaseChange
  have hq : Etale q := MorphismProperty.of_isPullback
    (P := (@Etale : MorphismProperty Scheme.{u})) H hfiber.1
  have hring : Algebra.Etale k C := RingHom.etale_algebraMap.mp
    ((HasRingHomProperty.Spec_iff (P := (@Etale : MorphismProperty Scheme.{u}))).mp hq)
  have : Module.Finite k C := Algebra.FormallyUnramified.finite_of_free k C
  let z : Spec (CommRingCat.of k) := IsLocalRing.closedPoint (CommRingCat.of k)
  let zX : Spec (X.residueField x) := IsLocalRing.closedPoint (X.residueField x)
  have hrank : q.finrank z = g.finrank zX :=
    (Scheme.Hom.finrank_of_isPullback _ q g a H z).trans
      (congrArg g.finrank (Subsingleton.elim (a z) zX))
  refine ⟨hring, hfiber.2.trans_eq ?_⟩
  calc
    g.finrank zX = q.finrank z := hrank.symm
    _ = Module.rankAtStalk C (IsLocalRing.closedPoint (CommRingCat.of k)) :=
      Scheme.Hom.finrank_SpecMap_algebraMap k C _
    _ = Module.finrank k C := by
      simp only [Module.rankAtStalk_eq_finrank_of_free, Pi.natCast_apply, Nat.cast_id]

theorem

finiteEtale_normalization_of_fiber_etale_degree

L125 ↗

EtaleFundamentalGroups.finiteEtale_normalization_of_fiber_etale_degree

Documentation

Original Tag 0BTF (8) ⇒ (4): étaleness and the original degree lower bound on every actual scheme-theoretic fiber imply global finite étaleness of the same normalization, for an arbitrary finite function-field extension.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

Lean source · statement

theorem finiteEtale_normalization_of_fiber_etale_degree
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L]
    [FiniteDimensional X.functionField L]
    (hfiber : ∀ x : X,
      Etale ((X.genericExtensionMorphism L).fromNormalization.fiberToSpecResidueField x) ∧
        Module.finrank X.functionField L ≤
          ((X.genericExtensionMorphism L).fromNormalization.fiberToSpecResidueField x).finrank
            (IsLocalRing.closedPoint (X.residueField x))) :
    IsFinite (X.genericExtensionMorphism L).fromNormalization ∧
      Etale (X.genericExtensionMorphism L).fromNormalization

GlobalFiberDegreeCriterion.lean

Module documentation

The original scheme-theoretic fiber degree criterion for normalization

fieldSpecQuasiCompact

normalizationChart_fiber_degree

finiteEtale_normalization_of_fiber_etale_degree

Module documentation

The original scheme-theoretic fiber degree criterion for normalization

Declarations

fieldSpecQuasiCompact

normalizationChart_fiber_degree

finiteEtale_normalization_of_fiber_etale_degree