EtaleFundamentalGroups.Kummer.finiteEtale_samePrime_boundaryAway_of_global_finite_henselianPushout
A global primitive Away map survives a finite Henselian pushout and localization at the exact mapped closed prime.
Unlike finiteEtale_samePrime_boundaryAway_of_finite_henselianPushout, the input is the map to the global finite-etale algebra E, not to E_p. Consequently no finiteness or etaleness assertion for the non-Henselian localization E_p is needed.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped BigOperators TensorProduct
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
universe uA₀ uB₀ uA uELean source · full declaration
theorem
finiteEtale_samePrime_boundaryAway_of_global_finite_henselianPushout
{A₀ : Type uA₀} {B₀ : Type uB₀}
{A : Type uA} {B : Type*} {E : Type uE}
[CommRing A₀] [CommRing B₀] [CommRing A] [CommRing B]
[CommRing E]
[IsNoetherianRing A]
[IsLocalRing B₀] [HenselianLocalRing B]
[Algebra A₀ B₀] [Algebra A₀ A]
[Algebra A₀ B] [Algebra A B] [Algebra B₀ B]
[IsScalarTower A₀ B₀ B] [IsScalarTower A₀ A B]
[Algebra.IsPushout A₀ B₀ A B]
[IsLocalHom (algebraMap B₀ B)]
[Module.FaithfullyFlat B₀ B]
[Module.Finite A₀ B₀]
[Algebra B₀ E] [Algebra A₀ E]
[IsScalarTower A₀ B₀ E]
[Module.Finite B₀ E] [Algebra.Etale B₀ E]
(p : Ideal E) [p.IsMaximal]
[p.LiesOver (maximalIdeal B₀)]
(hmax : (maximalIdeal B₀).map (algebraMap B₀ B) =
maximalIdeal B)
(hres : Function.Bijective
(IsLocalRing.ResidueField.map (algebraMap B₀ B)))
(f : A₀)
(hAway :
(Localization.awayMap (algebraMap A₀ E) f).Etale) :
let T := B ⊗[B₀] E
letI : Algebra E T := Algebra.TensorProduct.rightAlgebra
let p' := p.map (algebraMap E T)
let hp' : p'.IsMaximal :=
(tensorProduct_map_liesOver_maximalIdeal_of_residueFieldMap_bijective
(R := B₀) (R' := B) (S := E) p hmax hres).1
letI : p'.IsPrime := hp'.isPrime
let hp'Over : p'.LiesOver (maximalIdeal B) :=
(tensorProduct_map_liesOver_maximalIdeal_of_residueFieldMap_bijective
(R := B₀) (R' := B) (S := E) p hmax hres).2
letI : p'.LiesOver (maximalIdeal B) := hp'Over
let D := Localization.AtPrime p'
letI : CommRing D := OreLocalization.instCommRing
@Algebra.Etale
(Localization.Away (algebraMap A₀ A f))
(Localization.Away (algebraMap A D (algebraMap A₀ A f)))
(OreLocalization.instCommRing (R := A))
(OreLocalization.instCommRing (R := D))
(Localization.awayMap
(algebraMap A D) (algebraMap A₀ A f)).toAlgebra := by
dsimp only
let T := B ⊗[B₀] E
let : Algebra B T := Algebra.TensorProduct.leftAlgebra
let : Algebra E T := Algebra.TensorProduct.rightAlgebra
let : IsScalarTower B₀ B T := inferInstance
let : IsScalarTower B₀ E T :=
Algebra.TensorProduct.right_isScalarTower
let : Algebra A T := Algebra.TensorProduct.leftAlgebra
let : IsScalarTower A B T :=
TensorProduct.isScalarTower_left
let : Module.Finite A (A ⊗[A₀] B₀) :=
Module.Finite.base_change A₀ A B₀
let : Algebra.IsPushout A₀ A B₀ B :=
Algebra.IsPushout.symm
(inferInstance : Algebra.IsPushout A₀ B₀ A B)
let : Module.Finite A B :=
Module.Finite.equiv
(Algebra.IsPushout.equiv A₀ A B₀ B).toLinearEquiv
let p' := p.map (algebraMap E T)
have hgeometry :=
tensorProduct_map_liesOver_maximalIdeal_of_residueFieldMap_bijective
(R := B₀) (R' := B) (S := E) p hmax hres
let : p'.IsPrime := hgeometry.1.isPrime
let : p'.LiesOver (maximalIdeal B) := hgeometry.2
let D := Localization.AtPrime p'
let : Algebra T D := inferInstance
let : IsScalarTower B T D :=
OreLocalization.instIsScalarTower
have hTowerABD : IsScalarTower A B D :=
IsScalarTower.to₁₂₄ A B T D
let : Algebra A₀ T := Algebra.TensorProduct.leftAlgebra
let : IsScalarTower A₀ A T :=
IsScalarTower.to₁₂₄ A₀ A B T
let : IsScalarTower A₀ E T := by
apply IsScalarTower.of_algebraMap_eq
intro x
calc
algebraMap A₀ T x = algebraMap B T (algebraMap A₀ B x) :=
IsScalarTower.algebraMap_apply A₀ B T x
_ = algebraMap B T (algebraMap B₀ B (algebraMap A₀ B₀ x)) := by
rw [IsScalarTower.algebraMap_apply A₀ B₀ B]
_ = algebraMap B₀ T (algebraMap A₀ B₀ x) :=
(IsScalarTower.algebraMap_apply B₀ B T _).symm
_ = algebraMap E T (algebraMap B₀ E (algebraMap A₀ B₀ x)) :=
IsScalarTower.algebraMap_apply B₀ E T _
_ = algebraMap E T (algebraMap A₀ E x) := by
rw [IsScalarTower.algebraMap_apply A₀ B₀ E]
have hSecondPushout : Algebra.IsPushout B₀ E B T :=
(inferInstance : Algebra.IsPushout B₀ B E T).symm
have hTotalPushout : Algebra.IsPushout A₀ E A T :=
(Algebra.IsPushout.comp_iff A₀ B₀ A B).2 hSecondPushout
let : Algebra.IsPushout A₀ E A T := hTotalPushout
have hAwayBaseChange :
(Localization.awayMap
(algebraMap A T) (algebraMap A₀ A f)).Etale :=
localization_awayMap_etale_of_isPushout
(A := A₀) (B := E) (C := A) (D := T) f hAway
let : IsScalarTower A T D :=
IsScalarTower.to₁₃₄ A B T D
let : IsLocalization p'.primeCompl D := inferInstance
let : Algebra.FormallyEtale T D :=
Algebra.FormallyEtale.of_isLocalization p'.primeCompl
let : Module.Finite B D :=
moduleFinite_localizationAtPrime_of_henselian_of_etale p'
have hFiniteAD : Module.Finite A D :=
@Module.Finite.trans A B D _ _ _ _ _ _ hTowerABD
inferInstance inferInstance
let : Module.Finite A D := hFiniteAD
exact
localization_awayMap_etale_of_finite_formallyEtale_extension
(A := A) (C := T) (D := D)
(algebraMap A₀ A f) hAwayBaseChange