EtaleFundamentalGroups.Inertia.actualNormalizationResidueFieldMap_toQuotient
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 actualNormalizationResidueFieldMap_toQuotient
(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).carrier) [Q.IsMaximal]
(d : (normalizationDecompositionGroup A K L Q).carrier) (x : Q.ResidueField) :
(normalizationMaximalQuotientResidueEquiv A L Q).symm.toFun
((actualNormalizationResidueFieldMap A K L Q d).toFun x) =
((actualNormalizationQuotientAction A K L Q).toFun d).toFun
((normalizationMaximalQuotientResidueEquiv A L Q).symm.toFun x)