Module

BoundaryAway.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ChosenPrime.BoundaryAway

3 declarations indexed from sourceView source ↗

Module documentation

The primitive boundary Away map on the Tag 00UJ local factor

The boundary-complement hypothesis belongs to the original finite normalization. After the Tag 00UJ etale base change, it is first transported to the tensor product, then to the finite idempotent factor, and finally to the chosen prime-local factor. This construction never uses a root cover or a generic field component.

Imports3

Imported by4

theorem

isLocalization_localizationAtPrime_of_primesOver_eq_singleton

L36 ↗

EtaleFundamentalGroups.isLocalization_localizationAtPrime_of_primesOver_eq_singleton

Documentation

If q is the only prime of an integral algebra above p, then the prime-local ring at q is already the localization obtained by inverting the image of pᶜ.

The divisibility condition in the localization criterion is produced by integrality and uniqueness of the prime; it is not an additional comparison hypothesis.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uA uB

Lean source · statement

theorem isLocalization_localizationAtPrime_of_primesOver_eq_singleton
    {A : Type uA} {B : Type uB}
    [CommRing A] [CommRing B] [Algebra A B]
    {p : Ideal A} [p.IsPrime]
    {q : Ideal B} [q.IsPrime]
    [Algebra.IsIntegral A B]
    (hunique : p.primesOver B = {q}) :
    IsLocalization
      (Algebra.algebraMapSubmonoid B p.primeCompl)
      (Localization.AtPrime q)

theorem

etaleChosenAway_boundaryAway

L75 ↗

EtaleFundamentalGroups.etaleChosenAway_boundaryAway

Documentation

The primitive Away hypothesis on R → S survives passage to the finite Tag idempotent factor. Finiteness of that factor is exactly the production output of Tag 00UJ.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uA uB
universe uR uC uS

Lean source · statement

theorem etaleChosenAway_boundaryAway
    {R : Type uR} {C : Type uC} {S : Type uS}
    [CommRing R] [CommRing C] [CommRing S]
    [IsNoetherianRing C]
    [Algebra R C] [Algebra R S]
    (f : R)
    (hAway :
      (Localization.awayMap (algebraMap R S) f).Etale)
    (e : C ⊗[R] S)
    (hfinite : Module.Finite C (Localization.Away e)) :
    (Localization.awayMap
      (algebraMap C (Localization.Away e))
      (algebraMap R C f)).Etale

theorem

etaleChosenLocalFactor_pointed_boundaryAway

L109 ↗

EtaleFundamentalGroups.etaleChosenLocalFactor_pointed_boundaryAway

Documentation

The literal boundary Away map on the chosen Tag prime-local factor.

The singleton-fibre assertion supplied by Tag 00UJ makes the chosen local factor a pushout from the pointed base localization. Hence this conclusion is produced solely from the original normalization's Away hypothesis and the literal Tag data. In particular, no root cover, generic component, or comparison equivalence occurs in the statement.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uA uB
universe uR uC uS

Lean source · full declaration

theorem etaleChosenLocalFactor_pointed_boundaryAway
    {R : Type uR} {C : Type uC} {S : Type uS}
    [CommRing R] [CommRing C] [CommRing S]
    [IsNoetherianRing C]
    [Algebra R C] [Algebra R S]
    (f : R)
    (hAway :
      (Localization.awayMap (algebraMap R S) f).Etale)
    (P : Ideal C) [P.IsPrime]
    (e : C ⊗[R] S)
    (P' : Ideal (C ⊗[R] S))
    [P'.IsPrime] [P'.LiesOver P]
    (heP' : e ∉ P')
    (hfinite : Module.Finite C (Localization.Away e))
    (hunique : ∀ P'' : Ideal (C ⊗[R] S),
      P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P') :
    let Q := etaleChosenAwayPrime e P'
    letI : Q.IsPrime := etaleChosenAwayPrime_isPrime e P' heP'
    letI : Q.LiesOver P' := etaleChosenAwayPrime_liesOver e P' heP'
    letI : Q.LiesOver P := Ideal.LiesOver.trans Q P' P
    let Cₚ := Localization.AtPrime P
    let Dₚ := Localization.AtPrime Q
    letI : Algebra Cₚ Dₚ :=
      Localization.AtPrime.algebraOfLiesOver P Q
    @Algebra.Etale
      (Localization.Away
        (algebraMap C Cₚ (algebraMap R C f)))
      (Localization.Away
        (algebraMap Cₚ Dₚ
          (algebraMap C Cₚ (algebraMap R C f))))
      _ _
      (Localization.awayMap
        (algebraMap Cₚ Dₚ)
        (algebraMap C Cₚ (algebraMap R C f))).toAlgebra := by
  dsimp only
  let T := C ⊗[R] S
  let D := Localization.Away e
  let Q : Ideal D := etaleChosenAwayPrime e P'
  let : Q.IsPrime := etaleChosenAwayPrime_isPrime e P' heP'
  let : Q.LiesOver P' := etaleChosenAwayPrime_liesOver e P' heP'
  let : Q.LiesOver P := Ideal.LiesOver.trans Q P' P
  let Cₚ := Localization.AtPrime P
  let Dₚ := Localization.AtPrime Q
  let fC : C := algebraMap R C f
  let : Module.Finite C D := hfinite
  let : Algebra.IsIntegral C D := Algebra.IsIntegral.of_finite C D
  let : Algebra Cₚ Dₚ :=
    Localization.AtPrime.algebraOfLiesOver P Q
  have hQunique : P.primesOver D = {Q} :=
    etaleChosenAway_primesOver_eq_singleton
      P e P' heP' hunique
  let : IsLocalization
      (Algebra.algebraMapSubmonoid D P.primeCompl) Dₚ :=
    isLocalization_localizationAtPrime_of_primesOver_eq_singleton
      hQunique
  let : Algebra.IsPushout C D Cₚ Dₚ :=
    Algebra.isPushout_of_isLocalization P.primeCompl Cₚ D Dₚ
  have hD :
      (Localization.awayMap (algebraMap C D) fC).Etale :=
    etaleChosenAway_boundaryAway f hAway e hfinite
  exact
    localization_awayMap_etale_of_isPushout
      (A := C) (B := D) (C := Cₚ) (D := Dₚ) fC hD

Module documentation

The primitive boundary Away map on the Tag 00UJ local factor

Declarations

isLocalization_localizationAtPrime_of_primesOver_eq_singleton

etaleChosenAway_boundaryAway

etaleChosenLocalFactor_pointed_boundaryAway