EtaleFundamentalGroups.Inertia.originalFiniteNormalizationDecompositionMorphism_residue
The same original residue morphism factors through the actual normalization decomposition restriction and the intrinsic native residue morphism.
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 originalFiniteNormalizationDecompositionMorphism_residue
(A : Type u) (K : Type v) (F : Type w)
[CommRing A] [Field K] [Field F]
[Algebra A K] [IsFractionRing A K]
[Algebra K F] [Algebra A F] [IsScalarTower A K F] [IsGalois K F]
(Q : Ideal (normalizationCommAlgCat A F))
(d : normalizationDecompositionGroup A K F Q) :
(normalizationResidueMorphism A K F Q).hom'.toFun d =
(commAlgStabilizerResidueMorphism A (normalizationCommAlgCat A F) Q).hom'.toFun
((originalFiniteNormalizationDecompositionMorphism A K F Q).hom'.toFun d)