LocalClassFieldTheory.relativeNorm_coe_eq_of_closedSubgroup_eq
The underlying value of a relative norm is unchanged when its two closed-subgroup indices and its fixed coefficient are transported along equalities. Keeping this congruence explicit avoids dependent rewriting through the inclusion proof carried by relativeNorm.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology KummerTheory ClassFormation
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
[IsGalois K Ω] [IsSepClosed Ω]Lean source · statement
theorem relativeNorm_coe_eq_of_closedSubgroup_eq
{G : Type} [Group G] [TopologicalSpace G]
(A : Rep ℤ G)
(B B' C C' : ClosedSubgroup G)
(hCB : C.toSubgroup ≤ B.toSubgroup)
(hC'B' : C'.toSubgroup ≤ B'.toSubgroup)
[hfinite : Finite
(B.toSubgroup ⧸ extensionSubgroup B C hCB)]
[hfinite' : Finite
(B'.toSubgroup ⧸ extensionSubgroup B' C' hC'B')]
(hB : B = B') (hC : C = C')
(x : ambientFixedAddSubgroup A C)
(x' : ambientFixedAddSubgroup A C')
(hx : x.1 = x'.1) :
((relativeNorm A B C hCB x : ambientFixedAddSubgroup A B) : A.V) =
((relativeNorm A B' C' hC'B' x' :
ambientFixedAddSubgroup A B') : A.V)