NYLL
Module

Core.lean

Nyll.EtaleFundamentalGroups.Normalization.IntegralClosure.IntegralBase.ChosenLocalization.Core
2 declarations indexed from sourceView source ↗

Module documentation

A chosen local factor of one normalization after an integral base change

Let A → B be finite, with B Henselian local, and let both rings act on one ambient field L. The integral closures over A and B are the same subring of L; IntegralClosureIntegralBaseEquiv equips that literal A-normalization with its canonical B-algebra structure.

If the normalization is etale over B, localization at a chosen prime over the closed point is a finite etale local factor. Its maximal ideal is the unique prime over the closed point. This file also transports an independently given primitive A-away hypothesis from the original normalization to this chosen factor. Thus the away hypothesis below is source data from the original finite normalization, not an etaleness assumption on the desired chosen factor.

Imports5
Imported by7

Declarations

theorem

localization_awayMap_etale_of_finite_formallyEtale_extension

L42 ↗
EtaleFundamentalGroups.localization_awayMap_etale_of_finite_formallyEtale_extension
Documentation

A finite formally-etale extension of an algebra already etale away from f remains etale after applying the literal away map from the original base. This is the map-level composition needed after selecting a finite local factor of a normalization.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
universe uA uB uC uD uL
Lean source · statement
theorem localization_awayMap_etale_of_finite_formallyEtale_extension
    {A : Type uA} {C : Type uC} {D : Type uD}
    [CommRing A] [CommRing C] [CommRing D]
    [IsNoetherianRing A]
    [Algebra A C] [Algebra C D] [Algebra A D]
    [IsScalarTower A C D]
    [Module.Finite A D] [Algebra.FormallyEtale C D]
    (f : A)
    (hAway : (Localization.awayMap (algebraMap A C) f).Etale) :
    (Localization.awayMap (algebraMap A D) f).Etale
theorem

integralClosure_integralBase_chosenLocalization_finiteEtale_unique_away

L133 ↗
EtaleFundamentalGroups.integralClosure_integralBase_chosenLocalization_finiteEtale_unique_away
Documentation

The chosen localization of the common normalization is a finite etale factor over the integral Henselian base, has one prime over the closed point, and retains the literal primitive A-away map.

The input hAway is exactly the boundary-complement hypothesis on the original A-normalization integralClosure A L. Etaleness, finiteness, closed-prime uniqueness, and the away property of the selected factor are all produced here; no comparison equivalence or endpoint property is an input.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
universe uA uB uC uD uL
Lean source · full declaration
theorem integralClosure_integralBase_chosenLocalization_finiteEtale_unique_away
    {A : Type uA} {B : Type uB} {L : Type uL}
    [CommRing A] [CommRing B] [Field L]
    [IsNoetherianRing A]
    [HenselianLocalRing B]
    [Algebra A B] [Module.Finite A B]
    [Algebra A L] [Algebra B L] [IsScalarTower A B L]
    (hEtale : Algebra.Etale B (integralClosure B L))
    (f : A)
    (hAway :
      (Localization.awayMap
        (algebraMap A (integralClosure A L)) f).Etale) :
    let C := integralClosure A L
    letI : Algebra B C := integralClosureIntegralBaseAlgebra
    letI : IsScalarTower A B C :=
      integralClosureIntegralBase_isScalarTower
    ∀ (q : Ideal C) [q.IsPrime]
      [q.LiesOver (maximalIdeal B)],
      let D := Localization.AtPrime q
      Module.Finite B D ∧
        Algebra.Etale B D ∧
        (maximalIdeal D).LiesOver (maximalIdeal B) ∧
        (∀ Q : Ideal D, Q.IsPrime →
          Q.LiesOver (maximalIdeal B) → Q = maximalIdeal D) ∧
        @Algebra.Etale
          (Localization.Away f)
          (Localization.Away
            (algebraMap A D f))
          _ _
          (Localization.awayMap
            (algebraMap A D) f).toAlgebra := by
  dsimp only
  let C := integralClosure A L
  let : Algebra B C := integralClosureIntegralBaseAlgebra
  let : IsScalarTower A B C :=
    integralClosureIntegralBase_isScalarTower
  let : Algebra.Etale B C :=
    integralClosure_etale_of_integralBase hEtale
  intro q _ _
  let D := Localization.AtPrime q
  /- The canonical localization algebras make `A → D` the localization of
  the original normalization map, and make it agree with `A → B → D`. -/
  let : IsScalarTower A B D :=
    IsScalarTower.of_algebraMap_eq
      (R := A) (S := B) (A := D) fun a ↦ by
        calc
          algebraMap A D a = algebraMap C D (algebraMap A C a) :=
            IsScalarTower.algebraMap_apply A C D a
          _ = algebraMap C D
              (algebraMap B C (algebraMap A B a)) := by
            rw [IsScalarTower.algebraMap_apply A B C a]
          _ = algebraMap B D (algebraMap A B a) :=
            (IsScalarTower.algebraMap_apply B C D
              (algebraMap A B a)).symm
  let : IsNoetherianRing B := IsNoetherianRing.of_finite A B
  let : Module.Finite B D :=
    moduleFinite_localizationAtPrime_of_henselian_of_etale q
  have hEtaleD : Algebra.Etale B D := by
    let : Module.FinitePresentation B D :=
      Module.finitePresentation_of_finite B D
    let : Algebra.FinitePresentation B D :=
      Algebra.FinitePresentation.of_finitePresentation B D
    exact
      { formallyEtale := inferInstance
        finitePresentation := inferInstance }
  let : Algebra.Etale B D := hEtaleD
  let : Module.Finite A D := Module.Finite.trans B D
  let : IsLocalHom (algebraMap B D) :=
    isLocalHom_algebraMap_localizationAtPrime_of_liesOver_maximalIdeal q
  have hclosedOver : (maximalIdeal D).LiesOver (maximalIdeal B) :=
    inferInstance
  have hunique : ∀ Q : Ideal D, Q.IsPrime →
      Q.LiesOver (maximalIdeal B) → Q = maximalIdeal D := by
    intro Q hQPrime hQOver
    let : Q.IsPrime := hQPrime
    let : Q.LiesOver (maximalIdeal B) := hQOver
    let : Algebra.IsIntegral B D := Algebra.IsIntegral.of_finite B D
    have hQMaximal : Q.IsMaximal :=
      Ideal.isMaximal_of_isIntegral_of_isMaximal_comap (algebraMap B D)
        (fun x ↦ Algebra.IsIntegral.isIntegral x) Q <| by
          rw [← Ideal.under_def, ← Q.over_def (maximalIdeal B)]
          exact IsLocalRing.maximalIdeal.isMaximal B
    exact IsLocalRing.eq_maximalIdeal hQMaximal
  have hAwayD :=
    localization_awayMap_etale_of_finite_formallyEtale_extension
      (A := A) (C := C) (D := D) f hAway
  exact ⟨inferInstance, hEtaleD, hclosedOver, hunique, hAwayD⟩

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.