MainTransfer.lean

def transferNormNaturalityIntermediateInclusion
    (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal] :
    (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') →*
      (K.toSubgroup ⧸ extensionSubgroup K L (hLK'.trans hK'K))

theorem transferNormNaturalityIntermediateInclusion_mk
    (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal]
    (k' : K'.toSubgroup) :
    transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K
        (QuotientGroup.mk k') =
      QuotientGroup.mk (Subgroup.inclusion hK'K k')

theorem transferNormNaturalityIntermediateInclusion_injective
    (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal] :
    Function.Injective
      (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K)

def transferNormNaturalityIntermediateSubgroup
    (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal] :
    Subgroup (K.toSubgroup ⧸
      extensionSubgroup K L (hLK'.trans hK'K))

def transferNormNaturalityIntermediateQuotientEquiv
    (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal] :
    (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') ≃*
      transferNormNaturalityIntermediateSubgroup K K' L hLK' hK'K

theorem transferNormNaturalityIntermediateQuotientEquiv_mk
    (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal]
    (k' : K'.toSubgroup) :
    (transferNormNaturalityIntermediateQuotientEquiv K K' L hLK' hK'K
      (QuotientGroup.mk k')).1 =
      QuotientGroup.mk (Subgroup.inclusion hK'K k')

theorem transferNormNaturalityFrobeniusIntermediate_map_restriction
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal] :
    (D.transferNormNaturalityFrobeniusIntermediateSubgroup
        E L hL).map
        (D.extensionRestriction E.base.field L (hL.trans E.below)) =
      transferNormNaturalityIntermediateSubgroup
        E.base.field E.field.field L hL E.below

def transferNormNaturalityTransfer
    (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal]
    [Finite (K.toSubgroup ⧸
      extensionSubgroup K L (hLK'.trans hK'K))] :
    Abelianization (K.toSubgroup ⧸
        extensionSubgroup K L (hLK'.trans hK'K)) →*
      Abelianization (K'.toSubgroup ⧸ extensionSubgroup K' L hLK')

theorem transferNormNaturalityTransfer_restriction_natural
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal]
    [hLfinite : Finite
      (E.base.field.toSubgroup ⧸
        extensionSubgroup E.base.field L (hL.trans E.below))] :
    (transferNormNaturalityTransfer
        E.base.field E.field.field L hL E.below).comp
        (Abelianization.map
          (D.extensionRestriction E.base.field L (hL.trans E.below))) =
      (Abelianization.map
        (D.extensionRestriction E.field.field L hL)).comp
        (D.transferNormNaturalityFrobeniusTransfer E L hL)

theorem transferNormNaturalityTransfer_frobenius_product
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal]
    [Finite (E.base.field.toSubgroup ⧸
      extensionSubgroup E.base.field L (hL.trans E.below))]
    (σ : D.FrobeniusElements E.base L (hL.trans E.below)) :
    let H := D.transferNormNaturalityFrobeniusIntermediateSubgroup
      E L hL
    letI : H.FiniteIndex :=
      D.transferNormNaturalityFrobeniusIntermediateFiniteIndex
        E L hL
    let Ω := Quotient (orbitRel (Subgroup.zpowers σ.1)
      ((E.base.field.toSubgroup ⧸ D.extensionInertiaWithin E.base.field L
        (hL.trans E.below)) ⧸ H))
    letI : Fintype Ω := Fintype.ofFinite _
    transferNormNaturalityTransfer E.base.field E.field.field L hL E.below
        (Abelianization.of
          (D.frobeniusRestriction E.base L (hL.trans E.below) σ)) =
      ∏ q : Ω, Abelianization.of
        (D.frobeniusRestriction E.field L hL
          (D.transferNormNaturalityTransferFrobeniusLift
            E L hL σ q)) := by
  dsimp only
  let H := D.transferNormNaturalityFrobeniusIntermediateSubgroup
    E L hL
  let : H.FiniteIndex :=
    D.transferNormNaturalityFrobeniusIntermediateFiniteIndex
      E L hL
  let Ω := Quotient (orbitRel (Subgroup.zpowers σ.1)
    ((E.base.field.toSubgroup ⧸ D.extensionInertiaWithin E.base.field L
      (hL.trans E.below)) ⧸ H))
  let : Fintype Ω := Fintype.ofFinite _
  have hnat := D.transferNormNaturalityTransfer_restriction_natural
    E L hL
  have hnatσ := DFunLike.congr_fun hnat (Abelianization.of σ.1)
  have hprod := D.transferNormNaturalityFrobeniusTransfer_doubleCoset_formula
    E L hL σ.1
  calc
    transferNormNaturalityTransfer E.base.field E.field.field L hL E.below
        (Abelianization.of
          (D.frobeniusRestriction E.base L (hL.trans E.below) σ)) =
      Abelianization.map (D.extensionRestriction E.field.field L hL)
        (D.transferNormNaturalityFrobeniusTransfer E L hL
          (Abelianization.of σ.1)) := by
        simpa only [MonoidHom.comp_apply, Abelianization.map_of,
          DegreeData.frobeniusRestriction] using hnatσ
    _ = Abelianization.map (D.extensionRestriction E.field.field L hL)
        (∏ q : Ω, Abelianization.of
          ((D.transferNormNaturalityFrobeniusIntermediateEquiv
            E L hL).symm
              ⟨q.out.out⁻¹ * σ.1 ^ Function.minimalPeriod (σ.1 • ·) q.out *
                  q.out.out,
                QuotientGroup.out_conj_pow_minimalPeriod_mem
                  H σ.1 q.out⟩)) := by
        rw [hprod]
    _ = ∏ q : Ω, Abelianization.of
        (D.frobeniusRestriction E.field L hL
          (D.transferNormNaturalityTransferFrobeniusLift
            E L hL σ q)) := by
        rw [map_prod]
        apply Finset.prod_congr rfl
        intro q _
        rw [Abelianization.map_of]
        rfl

def transferNormNaturalityAbelianizedReciprocity
    (D : DegreeData G) (A : Rep ℤ G) (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (hAxiom : v.SatisfiesUnramifiedUnitCohomology D)
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    [hLfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)] :
    Additive (Abelianization
        (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)) →+
      FiniteNormQuotient A K.field L hLK

theorem transferNormNaturalityAbelianizedReciprocity_of
    (D : DegreeData G) (A : Rep ℤ G) (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (hAxiom : v.SatisfiesUnramifiedUnitCohomology D)
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    [hLfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (q : K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK) :
    D.transferNormNaturalityAbelianizedReciprocity A v hAxiom K L hLK
        (Additive.ofMul (Abelianization.of q)) =
      D.finiteReciprocityHom A v hAxiom K L hLK (Additive.ofMul q)

theorem transferNormNaturality_transfer_doubleCoset_formula
    (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [Finite (K.toSubgroup ⧸
      extensionSubgroup K L (hLK'.trans hK'K))]
    (σ : K.toSubgroup ⧸
      extensionSubgroup K L (hLK'.trans hK'K)) :
    letI : (extensionSubgroup K' L hLK').Normal :=
      transferNormNaturality_intermediateExtension_normal K K' L hLK' hK'K
    let H := transferNormNaturalityIntermediateSubgroup K K' L hLK' hK'K
    letI : H.FiniteIndex := Subgroup.finiteIndex_of_finite
    letI : Fintype (Quotient (orbitRel (Subgroup.zpowers σ)
        ((K.toSubgroup ⧸
          extensionSubgroup K L (hLK'.trans hK'K)) ⧸ H))) :=
      Fintype.ofFinite _
    transferNormNaturalityTransfer K K' L hLK' hK'K (Abelianization.of σ) =
      ∏ q : Quotient (orbitRel (Subgroup.zpowers σ)
          ((K.toSubgroup ⧸
            extensionSubgroup K L (hLK'.trans hK'K)) ⧸ H)),
        Abelianization.of
          ((transferNormNaturalityIntermediateQuotientEquiv K K' L hLK' hK'K).symm
            ⟨q.out.out⁻¹ * σ ^ Function.minimalPeriod (σ • ·) q.out *
                q.out.out,
              QuotientGroup.out_conj_pow_minimalPeriod_mem H σ q.out⟩) := by
  let hL'normal : (extensionSubgroup K' L hLK').Normal :=
    transferNormNaturality_intermediateExtension_normal K K' L hLK' hK'K
  dsimp only
  let H := transferNormNaturalityIntermediateSubgroup K K' L hLK' hK'K
  let : H.FiniteIndex := Subgroup.finiteIndex_of_finite
  let := Fintype.ofFinite
    (Quotient (orbitRel (Subgroup.zpowers σ)
      ((K.toSubgroup ⧸
        extensionSubgroup K L (hLK'.trans hK'K)) ⧸ H)))
  rw [transferNormNaturalityTransfer]
  simp only [MonoidHom.comp_apply, Abelianization.lift_apply_of]
  rw [MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot]
  rw [map_prod]
  apply Finset.prod_congr rfl
  intro q _
  exact abelianizationCongr_of
    (transferNormNaturalityIntermediateQuotientEquiv K K' L hLK' hK'K).symm _

def transferNormNaturalityExtensionFixedEquiv
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal) :
    (extensionFixedRepresentation A K L hLK hnormal).V ≃+
      ambientFixedAddSubgroup A L where
  toFun a := ⟨a.1, by
    intro l
    let s : extensionSubgroup K L hLK :=
      ⟨Subgroup.inclusion hLK l, l.2⟩
    exact a.2 s⟩
  invFun a := ⟨a.1, by
    rintro ⟨k, hk⟩
    exact a.2 ⟨k.1, hk⟩⟩
  left_inv _ := by rfl
  right_inv _ := by rfl
  map_add' _ _ := rfl

theorem transferNormNaturalityExtensionFixedEquiv_apply_coe
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    (a : (extensionFixedRepresentation A K L hLK hnormal).V) :
    ((transferNormNaturalityExtensionFixedEquiv A K L hLK hnormal a :
      ambientFixedAddSubgroup A L) : A.V) = a.1

theorem transferNormNaturalityExtensionFixedEquiv_symm_coe
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    (a : ambientFixedAddSubgroup A L) :
    ((transferNormNaturalityExtensionFixedEquiv A K L hLK hnormal).symm a).1 =
      a.1

def chosenTransferNormNaturalityRightTransversal
    (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal] :
    (transferNormNaturalityIntermediateSubgroup K K' L hLK' hK'K).RightTransversal

def transferNormNaturalityRightCosetProductEquiv
    (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal] :
    (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') ×
        (chosenTransferNormNaturalityRightTransversal K K' L hLK' hK'K :
          Set (K.toSubgroup ⧸
            extensionSubgroup K L (hLK'.trans hK'K))) ≃
      (K.toSubgroup ⧸ extensionSubgroup K L (hLK'.trans hK'K))

theorem transferNormNaturalityRightCosetProductEquiv_apply
    (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal]
    (r : K'.toSubgroup ⧸ extensionSubgroup K' L hLK')
    (t : (chosenTransferNormNaturalityRightTransversal K K' L hLK' hK'K :
      Set (K.toSubgroup ⧸
        extensionSubgroup K L (hLK'.trans hK'K)))) :
    transferNormNaturalityRightCosetProductEquiv K K' L hLK' hK'K (r, t) =
      transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K r * t.1

theorem transferNormNaturality_relativeCosetAction_eq_extensionAction
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    (a : (extensionFixedRepresentation A K L hLK hnormal).V)
    (q : K.toSubgroup ⧸ extensionSubgroup K L hLK) :
    relativeCosetAction A K L hLK
        (transferNormNaturalityExtensionFixedEquiv A K L hLK hnormal a) q =
      ((extensionFixedRepresentation A K L hLK hnormal).ρ q a).1

theorem transferNormNaturality_relativeCosetAction_intermediate
    (A : Rep ℤ G) (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal]
    (a : (extensionFixedRepresentation A K L
      (hLK'.trans hK'K) hLnormal).V)
    (r : K'.toSubgroup ⧸ extensionSubgroup K' L hLK') :
    relativeCosetAction A K' L hLK'
        (transferNormNaturalityExtensionFixedEquiv A K L
          (hLK'.trans hK'K) hLnormal a) r =
      ((extensionFixedRepresentation A K L
        (hLK'.trans hK'K) hLnormal).ρ
          (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K r) a).1

def transferNormNaturalityNormWitness
    (A : Rep ℤ G) (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal]
    [Finite (K.toSubgroup ⧸
      extensionSubgroup K L (hLK'.trans hK'K))]
    (a : ambientFixedAddSubgroup A L) :
    ambientFixedAddSubgroup A L

theorem transferNormNaturality_extensionAction_product
    (A : Rep ℤ G) (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal]
    (a : (extensionFixedRepresentation A K L
      (hLK'.trans hK'K) hLnormal).V)
    (r : K'.toSubgroup ⧸ extensionSubgroup K' L hLK')
    (t : (chosenTransferNormNaturalityRightTransversal K K' L hLK' hK'K :
      Set (K.toSubgroup ⧸
        extensionSubgroup K L (hLK'.trans hK'K)))) :
    (extensionFixedRepresentation A K L
        (hLK'.trans hK'K) hLnormal).ρ
        (transferNormNaturalityRightCosetProductEquiv K K' L hLK' hK'K (r, t)) a =
      (extensionFixedRepresentation A K L
        (hLK'.trans hK'K) hLnormal).ρ
        (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K r)
        ((extensionFixedRepresentation A K L
          (hLK'.trans hK'K) hLnormal).ρ t.1 a)

theorem transferNormNaturality_norm_doubleCoset_formula
    (A : Rep ℤ G) (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [Finite (K.toSubgroup ⧸
      extensionSubgroup K L (hLK'.trans hK'K))]
    (a : ambientFixedAddSubgroup A L) :
    letI : (extensionSubgroup K' L hLK').Normal :=
      transferNormNaturality_intermediateExtension_normal K K' L hLK' hK'K
    letI : Finite (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') :=
      Finite.of_injective
        (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K)
        (transferNormNaturalityIntermediateInclusion_injective
          K K' L hLK' hK'K)
    fixedFieldInclusion A K K' hK'K
        (relativeNorm A K L (hLK'.trans hK'K) a) =
      relativeNorm A K' L hLK'
        (transferNormNaturalityNormWitness A K K' L hLK' hK'K a) := by
  let hL'normal : (extensionSubgroup K' L hLK').Normal :=
    transferNormNaturality_intermediateExtension_normal K K' L hLK' hK'K
  let hL'finite : Finite
      (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') :=
    Finite.of_injective
      (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K)
      (transferNormNaturalityIntermediateInclusion_injective
        K K' L hLK' hK'K)
  let : Fintype (K.toSubgroup ⧸
      extensionSubgroup K L (hLK'.trans hK'K)) := Fintype.ofFinite _
  let : Fintype (K'.toSubgroup ⧸
      extensionSubgroup K' L hLK') := Fintype.ofFinite _
  let H := transferNormNaturalityIntermediateSubgroup K K' L hLK' hK'K
  let T := chosenTransferNormNaturalityRightTransversal K K' L hLK' hK'K
  let : H.FiniteIndex := Subgroup.finiteIndex_of_finite
  let : Fintype (T : Set (K.toSubgroup ⧸
      extensionSubgroup K L (hLK'.trans hK'K))) :=
    T.2.finite_right.fintype
  let E := extensionFixedRepresentation A K L
    (hLK'.trans hK'K) hLnormal
  let eA := transferNormNaturalityExtensionFixedEquiv A K L
    (hLK'.trans hK'K) hLnormal
  let aE := eA.symm a
  let valHom : E.V →+ A.V :=
    (ambientFixedAddSubgroup A L).subtype.comp eA.toAddMonoidHom
  apply Subtype.ext
  simp only [fixedFieldInclusion_coe, relativeNorm_apply_coe,
    relativeNormValue]
  have ha : eA aE = a := eA.apply_symm_apply a
  have hwitness :
      eA.symm (transferNormNaturalityNormWitness A K K' L hLK' hK'K a) =
        ∑ t : (T : Set (K.toSubgroup ⧸
          extensionSubgroup K L (hLK'.trans hK'K))), E.ρ t.1 aE := by
    simp [transferNormNaturalityNormWitness, T, E, eA, aE]
  have hE :
      (∑ q : K.toSubgroup ⧸
          extensionSubgroup K L (hLK'.trans hK'K), E.ρ q aE) =
        ∑ r : K'.toSubgroup ⧸ extensionSubgroup K' L hLK',
          E.ρ (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K r)
            (∑ t : (T : Set (K.toSubgroup ⧸
              extensionSubgroup K L (hLK'.trans hK'K))), E.ρ t.1 aE) := by
    calc
      (∑ q : K.toSubgroup ⧸
          extensionSubgroup K L (hLK'.trans hK'K), E.ρ q aE) =
          ∑ p : (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') ×
              (T : Set (K.toSubgroup ⧸
                extensionSubgroup K L (hLK'.trans hK'K))),
            E.ρ (transferNormNaturalityRightCosetProductEquiv
              K K' L hLK' hK'K p) aE :=
        (transferNormNaturalityRightCosetProductEquiv K K' L hLK' hK'K).sum_comp
          (fun q => E.ρ q aE) |>.symm
      _ = ∑ p : (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') ×
              (T : Set (K.toSubgroup ⧸
                extensionSubgroup K L (hLK'.trans hK'K))),
            E.ρ (transferNormNaturalityIntermediateInclusion
              K K' L hLK' hK'K p.1) (E.ρ p.2.1 aE) := by
        apply Fintype.sum_congr
        intro p
        exact transferNormNaturality_extensionAction_product
          A K K' L hLK' hK'K aE p.1 p.2
      _ = ∑ r : K'.toSubgroup ⧸ extensionSubgroup K' L hLK',
            ∑ t : (T : Set (K.toSubgroup ⧸
              extensionSubgroup K L (hLK'.trans hK'K))),
              E.ρ (transferNormNaturalityIntermediateInclusion
                K K' L hLK' hK'K r) (E.ρ t.1 aE) := by
        rw [Fintype.sum_prod_type]
      _ = ∑ r : K'.toSubgroup ⧸ extensionSubgroup K' L hLK',
          E.ρ (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K r)
            (∑ t : (T : Set (K.toSubgroup ⧸
              extensionSubgroup K L (hLK'.trans hK'K))), E.ρ t.1 aE) := by
        apply Fintype.sum_congr
        intro r
        rw [map_sum]
  calc
    (∑ q : K.toSubgroup ⧸
        extensionSubgroup K L (hLK'.trans hK'K),
      relativeCosetAction A K L (hLK'.trans hK'K) a q) =
        ∑ q : K.toSubgroup ⧸
          extensionSubgroup K L (hLK'.trans hK'K), (E.ρ q aE).1 := by
      apply Fintype.sum_congr
      intro q
      rw [← ha]
      exact transferNormNaturality_relativeCosetAction_eq_extensionAction
        A K L (hLK'.trans hK'K) hLnormal aE q
    _ = (∑ q : K.toSubgroup ⧸
        extensionSubgroup K L (hLK'.trans hK'K), E.ρ q aE).1 := by
      change (∑ q, valHom (E.ρ q aE)) = valHom (∑ q, E.ρ q aE)
      rw [map_sum]
    _ = (∑ r : K'.toSubgroup ⧸ extensionSubgroup K' L hLK',
        E.ρ (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K r)
          (∑ t : (T : Set (K.toSubgroup ⧸
            extensionSubgroup K L (hLK'.trans hK'K))), E.ρ t.1 aE)).1 :=
      congrArg Subtype.val hE
    _ = ∑ r : K'.toSubgroup ⧸ extensionSubgroup K' L hLK',
        (E.ρ (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K r)
          (∑ t : (T : Set (K.toSubgroup ⧸
            extensionSubgroup K L (hLK'.trans hK'K))), E.ρ t.1 aE)).1 := by
      change valHom (∑ r,
          E.ρ (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K r)
            (∑ t : (T : Set (K.toSubgroup ⧸
              extensionSubgroup K L (hLK'.trans hK'K))), E.ρ t.1 aE)) =
        ∑ r, valHom
          (E.ρ (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K r)
            (∑ t : (T : Set (K.toSubgroup ⧸
              extensionSubgroup K L (hLK'.trans hK'K))), E.ρ t.1 aE))
      rw [map_sum]
    _ = ∑ r : K'.toSubgroup ⧸ extensionSubgroup K' L hLK',
        relativeCosetAction A K' L hLK'
          (transferNormNaturalityNormWitness A K K' L hLK' hK'K a) r := by
      apply Fintype.sum_congr
      intro r
      rw [← hwitness]
      have hr := transferNormNaturality_relativeCosetAction_intermediate
        A K K' L hLK' hK'K
        (eA.symm (transferNormNaturalityNormWitness A K K' L hLK' hK'K a)) r
      calc
        _ = relativeCosetAction A K' L hLK'
            (eA (eA.symm
              (transferNormNaturalityNormWitness A K K' L hLK' hK'K a))) r := by
          simpa only [E, eA] using hr.symm
        _ = relativeCosetAction A K' L hLK'
            (transferNormNaturalityNormWitness A K K' L hLK' hK'K a) r := by
          rw [eA.apply_symm_apply]

def transferNormNaturalityNormQuotientInclusion
    (A : Rep ℤ G) (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [hL'normal : (extensionSubgroup K' L hLK').Normal]
    [Finite (K.toSubgroup ⧸
      extensionSubgroup K L (hLK'.trans hK'K))] :
    letI : Finite (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') :=
      Finite.of_injective
        (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K)
        (transferNormNaturalityIntermediateInclusion_injective
          K K' L hLK' hK'K)
    FiniteNormQuotient A K L (hLK'.trans hK'K) →+
      FiniteNormQuotient A K' L hLK' := by
  letI hL'finite : Finite
      (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') :=
    Finite.of_injective
      (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K)
      (transferNormNaturalityIntermediateInclusion_injective
        K K' L hLK' hK'K)
  let targetClass : ambientFixedAddSubgroup A K →+
      FiniteNormQuotient A K' L hLK' :=
    (finiteNormClassHom A K' L hLK').comp
      (fixedFieldInclusion A K K' hK'K)
  refine finiteNormQuotientLift A K L (hLK'.trans hK'K) targetClass ?_
  rintro _ ⟨a, rfl⟩
  apply (finiteNormClass_eq_zero_iff A K' L hLK' _).2
  refine ⟨transferNormNaturalityNormWitness A K K' L hLK' hK'K a, ?_⟩
  exact (transferNormNaturality_norm_doubleCoset_formula
    A K K' L hLK' hK'K a).symm

theorem transferNormNaturality_normQuotientInclusion_finiteNormClass
    (A : Rep ℤ G) (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal]
    [Finite (K.toSubgroup ⧸
      extensionSubgroup K L (hLK'.trans hK'K))]
    (x : ambientFixedAddSubgroup A K) :
    letI : (extensionSubgroup K' L hLK').Normal :=
      transferNormNaturality_intermediateExtension_normal K K' L hLK' hK'K
    letI : Finite (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') :=
      Finite.of_injective
        (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K)
        (transferNormNaturalityIntermediateInclusion_injective
          K K' L hLK' hK'K)
    transferNormNaturalityNormQuotientInclusion A K K' L hLK' hK'K
        (finiteNormClass A K L (hLK'.trans hK'K) x) =
      finiteNormClass A K' L hLK'
        (fixedFieldInclusion A K K' hK'K x) := by
  let hL'normal : (extensionSubgroup K' L hLK').Normal :=
    transferNormNaturality_intermediateExtension_normal K K' L hLK' hK'K
  let hL'finite : Finite
      (K'.toSubgroup ⧸ extensionSubgroup K' L hLK') :=
    Finite.of_injective
      (transferNormNaturalityIntermediateInclusion K K' L hLK' hK'K)
      (transferNormNaturalityIntermediateInclusion_injective
        K K' L hLK' hK'K)
  unfold transferNormNaturalityNormQuotientInclusion
  rw [finiteNormQuotientLift_finiteNormClass]
  rfl

theorem transferNormNaturality_generator_square
    (D : DegreeData G) (A : Rep ℤ G) (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (hAxiom : v.SatisfiesUnramifiedUnitCohomology D)
    (F : FiniteAbstractFieldExtension G) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ F.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup F.base.field L (hL.trans F.below)).Normal]
    [hLbasefinite : Finite (F.base.field.toSubgroup ⧸
      extensionSubgroup F.base.field L (hL.trans F.below))]
    (σ : D.FrobeniusElements
      (F.toFiniteResidueAbstractExtension D).base L
      (hL.trans F.below) (hLnormal := by
        change (extensionSubgroup F.base.field L
          (hL.trans F.below)).Normal
        exact hLnormal)) :
    letI : (extensionSubgroup F.field.field L hL).Normal :=
      transferNormNaturality_intermediateExtension_normal
        F.base.field F.field.field L hL F.below
    letI : Finite
        (F.field.field.toSubgroup ⧸
          extensionSubgroup F.field.field L hL) :=
      Finite.of_injective
        (transferNormNaturalityIntermediateInclusion
          F.base.field F.field.field L hL F.below)
        (transferNormNaturalityIntermediateInclusion_injective
          F.base.field F.field.field L hL F.below)
    D.transferNormNaturalityAbelianizedReciprocity A v hAxiom
        F.field L hL
        (Additive.ofMul
          (transferNormNaturalityTransfer
            F.base.field F.field.field L hL F.below
            (Abelianization.of
              (D.frobeniusRestriction
                (F.base.toFiniteResidueAbstractField D) L
                (hL.trans F.below) σ)))) =
      transferNormNaturalityNormQuotientInclusion A
        F.base.field F.field.field L hL F.below
        (D.transferNormNaturalityAbelianizedReciprocity A v hAxiom
          F.base L (hL.trans F.below)
          (Additive.ofMul
            (Abelianization.of
              (D.frobeniusRestriction
                (F.base.toFiniteResidueAbstractField D) L
                (hL.trans F.below) σ)))) := by
  let hL'normal : (extensionSubgroup F.field.field L hL).Normal :=
    transferNormNaturality_intermediateExtension_normal
      F.base.field F.field.field L hL F.below
  let hL'finite : Finite
      (F.field.field.toSubgroup ⧸
        extensionSubgroup F.field.field L hL) :=
    Finite.of_injective
      (transferNormNaturalityIntermediateInclusion
        F.base.field F.field.field L hL F.below)
      (transferNormNaturalityIntermediateInclusion_injective
        F.base.field F.field.field L hL F.below)
  let E := F.toFiniteResidueAbstractExtension D
  let hLnormalE :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal := by
    change (extensionSubgroup F.base.field L
      (hL.trans F.below)).Normal
    exact hLnormal
  let hL'normalE : (extensionSubgroup E.field.field L hL).Normal := by
    change (extensionSubgroup F.field.field L hL).Normal
    exact hL'normal
  let hLbasefiniteE : Finite (E.base.field.toSubgroup ⧸
      extensionSubgroup E.base.field L (hL.trans E.below)) := by
    change Finite (F.base.field.toSubgroup ⧸
      extensionSubgroup F.base.field L (hL.trans F.below))
    exact hLbasefinite
  let hL'finiteE : Finite (E.field.field.toSubgroup ⧸
      extensionSubgroup E.field.field L hL) := by
    change Finite (F.field.field.toSubgroup ⧸
      extensionSubgroup F.field.field L hL)
    exact hL'finite
  let S := D.frobeniusFixedField E.base L (hL.trans E.below) σ
  let hSK := D.frobeniusFixedField_le E.base L (hL.trans E.below) σ
  let hSKF : S.toSubgroup ≤ F.base.field.toSubgroup := by
    change S.toSubgroup ≤ E.base.field.toSubgroup
    exact hSK
  let : Finite (E.base.field.toSubgroup ⧸
      extensionSubgroup E.base.field S hSK) :=
    D.frobeniusFixedField_finite E.base L (hL.trans E.below) σ
  let hSbasefiniteF : Finite (F.base.field.toSubgroup ⧸
      extensionSubgroup F.base.field S hSKF) := by
    change Finite (E.base.field.toSubgroup ⧸
      extensionSubgroup E.base.field S hSK)
    infer_instance
  let Sfinite : FiniteAbstractField G := {
    field := S
    finite := by
      simpa [E, S,
        FiniteAbstractFieldExtension.toFiniteResidueAbstractExtension,
        FiniteAbstractField.toFiniteResidueAbstractField] using
        D.frobeniusFixedField_absoluteFinite F.base L
          (hL.trans F.below) σ }
  let π : ambientFixedAddSubgroup A S := v.chosenPrimeElement Sfinite
  let H := D.transferNormNaturalityFrobeniusIntermediateSubgroup
    E L hL
  let : H.FiniteIndex :=
    D.transferNormNaturalityFrobeniusIntermediateFiniteIndex
      E L hL
  let Ω := Quotient (orbitRel (Subgroup.zpowers σ.1)
    ((E.base.field.toSubgroup ⧸ D.extensionInertiaWithin E.base.field L
      (hL.trans E.below)) ⧸ H))
  let : Fintype Ω := Fintype.ofFinite _
  let β (q : Ω) := D.transferNormNaturalityTransferFrobeniusLift
    E L hL σ q
  let tK (q : Ω) : E.base.field.toSubgroup := Quotient.out q.out.out
  let C (q : Ω) := conjugateClosedSubgroup S (tK q).1
  let Sβ (q : Ω) := D.frobeniusFixedField E.field L hL (β q)
  let hSβK' (q : Ω) :=
    D.frobeniusFixedField_le E.field L hL (β q)
  let hSβK'F (q : Ω) : (Sβ q).toSubgroup ≤
      F.field.field.toSubgroup := by
    change (Sβ q).toSubgroup ≤ E.field.field.toSubgroup
    exact hSβK' q
  let hSβC (q : Ω) : (Sβ q).toSubgroup ≤ (C q).toSubgroup :=
    D.transferNormNaturalityTransferFrobenius_fixedField_le_conjugate
      E L hL σ q
  let πβ (q : Ω) : ambientFixedAddSubgroup A (Sβ q) :=
    fixedFieldInclusion A (C q) (Sβ q) (hSβC q)
      (conjugateFixedElement A S (tK q).1 π)
  let (q : Ω) : Finite
      (E.field.field.toSubgroup ⧸
        extensionSubgroup E.field.field (Sβ q) (hSβK' q)) :=
    D.frobeniusFixedField_finite E.field L hL (β q)
  let (q : Ω) : Finite
      (F.field.field.toSubgroup ⧸
        extensionSubgroup F.field.field (Sβ q) (hSβK'F q)) := by
    change Finite
      (E.field.field.toSubgroup ⧸
        extensionSubgroup E.field.field (Sβ q) (hSβK' q))
    infer_instance
  let (q : Ω) : Finite ((baseField G).toSubgroup ⧸
      extensionSubgroup (baseField G) (Sβ q) (le_baseField (Sβ q))) :=
    D.frobeniusFixedField_absoluteFinite F.field L hL (β q)
  let Sβfinite (q : Ω) : FiniteAbstractField G := {
    field := Sβ q
    finite := inferInstance }
  have hPrime (q : Ω) : v.IsPrimeElement (Sβfinite q) (πβ q) := by
    exact D.transferNormNaturalityTransferFrobenius_conjugatePrime_isPrime
      A v F L hL σ q π
        (v.chosenPrimeElement_isPrime Sfinite)
  let M := extensionSubgroup E.base.field E.field.field E.below
  let ΩN := Quotient (orbitRel M
    (E.base.field.toSubgroup ⧸ extensionSubgroup E.base.field S hSK))
  let orbitEquiv : Ω ≃ ΩN :=
    D.transferNormNaturalityTransferNormOrbitEquiv E L hL σ
  let : Fintype ΩN := Fintype.ofFinite _
  let f : ΩN → A.V := fun qN =>
    let q := orbitEquiv.symm qN
    ((relativeNorm A E.field.field (Sβ q) (hSβK' q) (πβ q) :
      ambientFixedAddSubgroup A E.field.field) : A.V)
  have hNorm0 := D.transferNormNaturalityNorm_eq_sum_transferNorms
    A F L hL σ π
  have hNorm :
      ((fixedFieldInclusion A E.base.field E.field.field E.below
          (relativeNorm A E.base.field S hSK π) :
            ambientFixedAddSubgroup A E.field.field) : A.V) =
        ∑ q : Ω, ((relativeNorm A E.field.field
          (Sβ q) (hSβK' q) (πβ q) :
            ambientFixedAddSubgroup A E.field.field) : A.V) := by
    calc
      _ = ∑ qN : ΩN, f qN := by
        simpa only [f, orbitEquiv, Sβ, hSβK', πβ, C, tK, β, S,
          hSK, E] using hNorm0
      _ = ∑ q : Ω, f (orbitEquiv q) :=
        (orbitEquiv.sum_comp f).symm
      _ = ∑ q : Ω, ((relativeNorm A E.field.field
          (Sβ q) (hSβK' q) (πβ q) :
            ambientFixedAddSubgroup A E.field.field) : A.V) := by
        apply Fintype.sum_congr
        intro q
        change ((relativeNorm A E.field.field
            (Sβ (orbitEquiv.symm (orbitEquiv q)))
            (hSβK' (orbitEquiv.symm (orbitEquiv q)))
            (πβ (orbitEquiv.symm (orbitEquiv q))) :
              ambientFixedAddSubgroup A E.field.field) : A.V) = _
        rw [orbitEquiv.symm_apply_apply]
  have hTransfer := D.transferNormNaturalityTransfer_frobenius_product
    E L hL σ
  change D.transferNormNaturalityAbelianizedReciprocity A v hAxiom
      F.field L hL
        (Additive.ofMul
          (transferNormNaturalityTransfer
            E.base.field E.field.field L hL E.below
            (Abelianization.of
              (D.frobeniusRestriction E.base L
                (hL.trans E.below) σ)))) = _
  rw [hTransfer]
  change D.transferNormNaturalityAbelianizedReciprocity A v hAxiom
      F.field L hL
        (∑ q : Ω, Additive.ofMul
          (Abelianization.of
            (D.frobeniusRestriction E.field L hL (β q)))) = _
  rw [map_sum]
  let hLnormalF :
      (extensionSubgroup F.base.field L (hL.trans F.below)).Normal :=
    hLnormal
  let hL'normalF : (extensionSubgroup F.field.field L hL).Normal :=
    hL'normal
  let hLbasefiniteF : Finite (F.base.field.toSubgroup ⧸
      extensionSubgroup F.base.field L (hL.trans F.below)) :=
    hLbasefinite
  let hL'finiteF : Finite (F.field.field.toSubgroup ⧸
      extensionSubgroup F.field.field L hL) :=
    hL'finite
  have hLeft :
      (∑ q : Ω,
        D.transferNormNaturalityAbelianizedReciprocity A v hAxiom
          F.field L hL
            (Additive.ofMul
              (Abelianization.of
                (D.frobeniusRestriction E.field L hL (β q))))) =
      ∑ q : Ω, finiteNormClass A F.field.field L hL
          (relativeNorm A F.field.field (Sβ q) (hSβK'F q) (πβ q)) := by
    apply Fintype.sum_congr
    intro q
    have hReciprocity :
        D.finiteReciprocityHom A v hAxiom F.field L hL
            (Additive.ofMul
              (D.frobeniusRestriction E.field L hL (β q))) =
          finiteNormClass A F.field.field L hL
            (relativeNorm A F.field.field (Sβ q) (hSβK'F q) (πβ q)) :=
      D.finiteReciprocityHom_apply_eq_primeNormClass
        A v hAxiom F.field L hL
        (Additive.ofMul
          (D.frobeniusRestriction E.field L hL (β q)))
        (β q) rfl (πβ q) (by
          simpa [Sβfinite, Sβ, E,
            FiniteAbstractFieldExtension.toFiniteResidueAbstractExtension,
            FiniteAbstractField.toFiniteResidueAbstractField] using hPrime q)
    exact (D.transferNormNaturalityAbelianizedReciprocity_of
      A v hAxiom F.field L hL
      (D.frobeniusRestriction E.field L hL (β q))).trans hReciprocity
  rw [hLeft]
  have hBase :
      D.transferNormNaturalityAbelianizedReciprocity A v hAxiom
          F.base L (hL.trans F.below)
          (Additive.ofMul
            (Abelianization.of
              (D.frobeniusRestriction (F.base.toFiniteResidueAbstractField D) L
                (hL.trans F.below) σ))) =
        finiteNormClass A F.base.field L (hL.trans F.below)
          (relativeNorm A F.base.field S hSKF π) :=
    (D.transferNormNaturalityAbelianizedReciprocity_of
      A v hAxiom F.base L (hL.trans F.below)
      (D.frobeniusRestriction (F.base.toFiniteResidueAbstractField D) L
        (hL.trans F.below) σ)).trans
      (D.finiteReciprocityHom_apply_eq_primeNormClass
        A v hAxiom F.base L (hL.trans F.below)
        (Additive.ofMul
          (D.frobeniusRestriction (F.base.toFiniteResidueAbstractField D) L
            (hL.trans F.below) σ))
        σ rfl π (v.chosenPrimeElement_isPrime Sfinite))
  have hRight := (congrArg
    (transferNormNaturalityNormQuotientInclusion A
      F.base.field F.field.field L hL F.below) hBase).trans
    (transferNormNaturality_normQuotientInclusion_finiteNormClass
      A F.base.field F.field.field L hL F.below
      (relativeNorm A F.base.field S hSKF π))
  have hNormSub :
      fixedFieldInclusion A E.base.field E.field.field E.below
          (relativeNorm A E.base.field S hSK π) =
        ∑ q : Ω,
          relativeNorm A E.field.field (Sβ q) (hSβK' q) (πβ q) := by
    apply Subtype.ext
    let valHom : ambientFixedAddSubgroup A E.field.field →+ A.V :=
      { toFun := fun x => x.1
        map_zero' := rfl
        map_add' := fun _ _ => rfl }
    change valHom (fixedFieldInclusion A E.base.field E.field.field E.below
        (relativeNorm A E.base.field S hSK π)) =
      valHom (∑ q : Ω,
        relativeNorm A E.field.field (Sβ q) (hSβK' q) (πβ q))
    rw [map_sum]
    exact hNorm
  have hNormSubF :
      fixedFieldInclusion A F.base.field F.field.field F.below
          (relativeNorm A F.base.field S hSKF π) =
        ∑ q : Ω,
          relativeNorm A F.field.field (Sβ q) (hSβK'F q) (πβ q) := by
    change fixedFieldInclusion A F.base.field F.field.field F.below
        (relativeNorm A F.base.field S hSKF π) =
      ∑ q : Ω,
        relativeNorm A F.field.field (Sβ q) (hSβK'F q) (πβ q) at hNormSub
    exact hNormSub
  have hNormClasses := congrArg
    (finiteNormClassHom A F.field.field L hL) hNormSubF
  rw [map_sum] at hNormClasses
  exact hNormClasses.symm.trans hRight.symm

theorem transferNormNaturality
    (D : DegreeData G) (A : Rep ℤ G) (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (hAxiom : v.SatisfiesUnramifiedUnitCohomology D)
    (F : FiniteAbstractFieldExtension G) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ F.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup F.base.field L (hL.trans F.below)).Normal]
    [hLbasefinite : Finite (F.base.field.toSubgroup ⧸
      extensionSubgroup F.base.field L (hL.trans F.below))] :
    letI : (extensionSubgroup F.field.field L hL).Normal :=
      transferNormNaturality_intermediateExtension_normal
        F.base.field F.field.field L hL F.below
    letI : Finite
        (F.field.field.toSubgroup ⧸
          extensionSubgroup F.field.field L hL) :=
      Finite.of_injective
        (transferNormNaturalityIntermediateInclusion
          F.base.field F.field.field L hL F.below)
        (transferNormNaturalityIntermediateInclusion_injective
          F.base.field F.field.field L hL F.below)
    (D.transferNormNaturalityAbelianizedReciprocity A v hAxiom
        F.field L hL).comp
      (MonoidHom.toAdditive
        (transferNormNaturalityTransfer
          F.base.field F.field.field L hL F.below)) =
      (transferNormNaturalityNormQuotientInclusion A
        F.base.field F.field.field L hL F.below).comp
        (D.transferNormNaturalityAbelianizedReciprocity A v hAxiom
          F.base L (hL.trans F.below)) := by
  let hL'normal : (extensionSubgroup F.field.field L hL).Normal :=
    transferNormNaturality_intermediateExtension_normal
      F.base.field F.field.field L hL F.below
  let : Finite
      (F.field.field.toSubgroup ⧸ extensionSubgroup F.field.field L hL) :=
    Finite.of_injective
      (transferNormNaturalityIntermediateInclusion
        F.base.field F.field.field L hL F.below)
      (transferNormNaturalityIntermediateInclusion_injective
        F.base.field F.field.field L hL F.below)
  apply AddMonoidHom.ext
  intro x
  change D.transferNormNaturalityAbelianizedReciprocity A v hAxiom
      F.field L hL
        (Additive.ofMul
          (transferNormNaturalityTransfer
            F.base.field F.field.field L hL F.below x.toMul)) =
    transferNormNaturalityNormQuotientInclusion A
      F.base.field F.field.field L hL F.below
      (D.transferNormNaturalityAbelianizedReciprocity A v hAxiom
        F.base L (hL.trans F.below) (Additive.ofMul x.toMul))
  refine QuotientGroup.induction_on x.toMul ?_
  intro q
  obtain ⟨σ, hσ⟩ := D.frobeniusRestriction_surjective
    (F.base.toFiniteResidueAbstractField D) L (hL.trans F.below) q
  rw [← hσ]
  exact D.transferNormNaturality_generator_square
    A v hAxiom F L hL σ