EtaleFundamentalGroups.Inertia.normalizationDVR_absolute_ramification
Every original-scope conclusion of Stacks Project, Lemma 58.13.6.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v wLean source · full declaration
theorem normalizationDVR_absolute_ramification
(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] :
NativeAbsoluteRamificationConclusions (actualAbsoluteRamificationResidues A Ω Q)
(actualAbsoluteRamificationGroups A K Ω Q) (actualAbsoluteRamificationDiagram A K Ω Q) where
residue_closure := actualAbsoluteRamificationResidueConclusions A K Ω Q
inertia_inclusion_injective := actualNormalizationInertiaToDecomposition_injective A K Ω Q
residue_kernel := (normalizationAbsoluteResidueMorphism_ker A K Ω Q).trans
(actualNormalizationResidueMorphism_ker A K Ω Q)
residue_surjective := normalizationAbsoluteResidueMorphism_surjective A K Ω Q
wild_inclusion_injective := Subtype.val_injective
wild_normal_in_decomposition := actualNormalizationWildSubgroup_normal_in_decomposition A K Ω Q
wild_pro_p := by
intro p hp hchar wildGroup wildTopology
change CharP (IsLocalRing.ResidueField A) p at hchar
exact ⟨actualNormalizationWildGroup_compactSpace A K Ω Q,
actualNormalizationWildGroup_t2Space A K Ω Q,
actualNormalizationWildGroup_totallyDisconnectedSpace A K Ω Q,
actualNormalizationWildGroup_isTopologicalGroup A K Ω Q,
actualNormalizationWildGroup_hasPGroupOpenNormalBasis A K Ω Q p⟩
wild_char_zero := by
intro hchar
change CharZero (IsLocalRing.ResidueField A) at hchar
exact actualNormalizationWildSubgroup_eq_bot_of_baseResidue_charZero A K Ω Q
character_continuous := actualAbsoluteTameCharacter_continuous A K Ω Q
character_surjective := actualAbsoluteTameCharacter_surjective A K Ω Q
character_kernel := actualAbsoluteTameCharacter_ker A K Ω Q
character_equivariant := actualAbsoluteTameCharacter_conjugate A K Ω Q
quotient_surjective := actualTameQuotientProjection_surjective A K Ω Q
quotient_kernel := actualTameQuotientProjection_ker A K Ω Q
quotient_isomorphism :=
⟨actualAbsoluteTameQuotientEquiv A K Ω Q, actualAbsoluteTameQuotientEquiv_projection A K Ω Q⟩