EtaleFundamentalGroups.Inertia.originalInertia_finiteNormalization_difference
Every element of the original actual inertia restricts to inertia at the literal finite normalization prime. The finite action and its square are constructed from actual restriction, with no comparison premise.
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 originalInertia_finiteNormalization_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 (integralClosure A L)) (E : FiniteGaloisIntermediateField K L)
(σ : actualNormalizationInertiaGroup A K L Q) :
∀ b : finiteAbsoluteNormalizationAlgebra A K L E,
(finiteAbsoluteNormalizationPrime A K L Q E).carrier
((actualFiniteNormalizationRestrictionRingHom A K L E
(actualNormalizationInertiaElement A K L Q σ)).toFun b - b)