EtaleFundamentalGroups.finiteTower_integralEtaleTarget_boundaryAway_of_local_awayMapsAtPrime
Globalize target-prime local Away maps for a literal composite through a finite algebra and an integral etale algebra.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe uR uD uCLean source · full declaration
theorem finiteTower_integralEtaleTarget_boundaryAway_of_local_awayMapsAtPrime
{R : Type uR} {D : Type uD} {C : Type uC}
[CommRing R] [CommRing D] [CommRing C]
[IsNoetherianRing R]
[Algebra D C] [Algebra.IsIntegral D C]
(mapRD : R →+* D)
(hfiniteRD :
letI : Algebra R D := mapRD.toAlgebra
Module.Finite R D)
(hEtale : Algebra.Etale D C)
(f : R)
(hlocal :
let mapRC : R →+* C :=
(algebraMap D C).comp mapRD
letI : Algebra R C := mapRC.toAlgebra
∀ (Q : Ideal C), [Q.IsPrime] →
mapRC f ∉ Q →
let p := Q.under R
letI : Algebra (Localization.AtPrime p) (Localization.AtPrime Q) :=
Localization.AtPrime.algebraOfLiesOver p Q
let fp : Localization.AtPrime p :=
algebraMap R (Localization.AtPrime p) f
(Localization.awayMap
(algebraMap (Localization.AtPrime p) (Localization.AtPrime Q))
fp).Etale) :
(Localization.awayMap
((algebraMap D C).comp mapRD) f).Etale := by
let : Algebra R D := mapRD.toAlgebra
let : Module.Finite R D := hfiniteRD
let mapRC : R →+* C :=
(algebraMap D C).comp mapRD
let : Algebra R C := mapRC.toAlgebra
let : IsScalarTower R D C := IsScalarTower.of_algebraMap_eq' rfl
let : Algebra.Etale D C := hEtale
let : Module.Finite D C := Algebra.IsIntegral.finite
let : Module.Finite R C := Module.Finite.trans D C
let : Module.FinitePresentation R C :=
Module.finitePresentation_of_finite R C
let : Algebra.FinitePresentation R C :=
Algebra.FinitePresentation.of_finitePresentation R C
exact ringHom_localization_awayMap_etale_of_local_awayMapsAtPrime
mapRC (by
change Algebra.FinitePresentation R C
infer_instance) f hlocal