EtaleFundamentalGroups.Inertia.normalizationAbsoluteResidueMorphism_commutes
Applying the original absolute residue morphism and then the coefficient inclusion is the same as applying the original literal quotient action.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v wLean source · statement
theorem normalizationAbsoluteResidueMorphism_commutes
(A : Type u) (K : Type v) (Ω : Type w)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
[Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
(Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
(d : (normalizationDecompositionGroup A K Ω Q).carrier)
(z : (nativeSeparableResidueField (IsLocalRing.ResidueField A)
(normalizationResidueFieldObject A Ω Q) (normalizationResidueFieldAlgebra A Ω Q)).α) :
nativeSeparableResidueActionScalar (IsLocalRing.ResidueField A)
(normalizationResidueFieldObject A Ω Q) (normalizationResidueFieldAlgebra A Ω Q)
((normalizationAbsoluteResidueMorphism A K Ω Q).hom'.toFun d) z =
actualNormalizationQuotientActionScalar A K Ω Q d
(nativeSeparableResidueScalar (IsLocalRing.ResidueField A)
(normalizationResidueFieldObject A Ω Q) (normalizationResidueFieldAlgebra A Ω Q) z)