EtaleFundamentalGroups.Inertia.integralClosure_inertia_fixed_finite_representatives
A finite set of inertia-fixed integral elements is represented at one actual finite Galois level, with literal inclusion equality and the genuine finite-level inertia action. Fixedness is descended using the proved equality of inertia images; no colimit or fixed-ring comparison is assumed.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTowerLean source · statement
theorem integralClosure_inertia_fixed_finite_representatives
(A : Type u) (K : Type v) (L : Type w)
[CommRing A] [Field K] [Field L]
[Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
(Q : Ideal (integralClosure A L)) [Q.IsPrime]
(s : Finset (integralClosure A L))
(hs : ∀ b ∈ s, ∀ σ ∈ Q.inertia Gal(L/K), σ • b = b) :
∃ E : FiniteGaloisIntermediateField K L,
∀ b ∈ s, ∃ bE : integralClosure A E,
(IsScalarTower.toAlgHom A E L).mapIntegralClosure bE = b ∧
∀ τ ∈ (Q.comap (IsScalarTower.toAlgHom A E L).mapIntegralClosure).inertia Gal(E/K),
τ • bE = bE