EtaleFundamentalGroups.Inertia.actualFiniteNormalizationRestriction_inertia_difference
Restriction of an actual ambient normalization inertia automorphism satisfies the inertia condition at the literal finite contraction. The coefficient square is proved by the actual restriction construction.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v wLean source · statement
theorem actualFiniteNormalizationRestriction_inertia_difference
(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 (normalizationCommAlgCat A L))
(E : FiniteGaloisIntermediateField K L) (σ : Gal(L/K))
(hσ : ∀ b : normalizationCommAlgCat A L,
normalizationGaloisRingHom A K L σ b - b ∈ Q) :
∀ b : finiteAbsoluteNormalizationAlgebra A K L E,
actualFiniteNormalizationRestrictionRingHom A K L E σ b - b ∈
finiteAbsoluteNormalizationPrime A K L Q E