Module

ClassFieldCandidate.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.ClassFieldCandidate

19 declarations indexed from sourceView source ↗

Module documentation

A finite class-field candidate from a norm-open subgroup

This file isolates the source-producing part of finite-classification surjectivity. An open subgroup H ≤ A_K contains an actual finite Galois norm subgroup. Modulo that norm subgroup, H gives a concrete subgroup. Transporting this subgroup to the additive abelianization and pulling it back along Q → Qᵃᵇ gives a subgroup of the actual finite Galois quotient which contains its commutator. The finite Galois correspondence then cuts out an actual finite abelian intermediate extension.

The equivalence used for the transport is an explicit argument of the construction. A later specialization supplies it from finite reciprocity for the reciprocity map. No existence statement, norm-kernel equality, or classification conclusion depending on that specialization is asserted here.

The finite level beneath an open norm-topology subgroup

Transport to the abelianized finite quotient

From a subgroup above the commutator to an abelian field

Imports4

Imported by3

theorem

normOpenAddSubgroup_contains_finiteNormSubgroup

L49 ↗

ClassFormation.normOpenAddSubgroup_contains_finiteNormSubgroup

Documentation

The first step in the proof of the finite abelian classification theorem: an open subgroup in the norm topology contains the norm subgroup of an actual finite Galois extension.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem normOpenAddSubgroup_contains_finiteNormSubgroup
    (A : Rep ℤ G) (K : ClosedSubgroup G)
    (H : AddSubgroup (ambientFixedAddSubgroup A K))
    (hH : IsNormOpen A K H) :
    ∃ E : FiniteGaloisSubextension K,
      ClassFormation.FiniteGaloisSubextension.normSubgroup A E ≤ H

instance

normQuotient_extensionQuotient_finite

L61 ↗

ClassFormation.FiniteGaloisSubextension.normQuotient_extensionQuotient_finite

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

instance normQuotient_extensionQuotient_finite
    (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below)

def

normQuotientSubgroup

L68 ↗

ClassFormation.FiniteGaloisSubextension.normQuotientSubgroup

Documentation

The subgroup H / N_E of the actual norm quotient, represented as the image of H under the quotient map.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
local instance normQuotient_extensionQuotient_finite
    (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite

Lean source · statement

def normQuotientSubgroup
    (A : Rep ℤ G) (E : FiniteGaloisSubextension K)
    (H : AddSubgroup (ambientFixedAddSubgroup A K)) :
    AddSubgroup (FiniteNormQuotient A K E.field E.below)

theorem

finiteNormClass_mem_normQuotientSubgroup_iff

L80 ↗

ClassFormation.FiniteGaloisSubextension.finiteNormClass_mem_normQuotientSubgroup_iff

Documentation

If N_E ⊆ H, then H is exactly the full inverse image of H / N_E. This is the group-theoretic fact used in the middle of the finite-classification surjectivity proof.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
local instance normQuotient_extensionQuotient_finite
    (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite
omit [IsTopologicalGroup G] in

Lean source · full declaration

theorem finiteNormClass_mem_normQuotientSubgroup_iff
    (A : Rep ℤ G) (E : FiniteGaloisSubextension K)
    (H : AddSubgroup (ambientFixedAddSubgroup A K))
    (hEH : ClassFormation.FiniteGaloisSubextension.normSubgroup A E ≤ H)
    (a : ambientFixedAddSubgroup A K) :
    letI : Finite (K.toSubgroup ⧸
        extensionSubgroup K E.field E.below) := E.finite
    finiteNormClass A K E.field E.below a ∈
        normQuotientSubgroup A E H ↔
      a ∈ H := by
  let : Finite (K.toSubgroup ⧸
      extensionSubgroup K E.field E.below) := E.finite
  constructor
  · rintro ⟨b, hb, hba⟩
    have hba' : finiteNormClass A K E.field E.below b =
        finiteNormClass A K E.field E.below a := by
      simpa [finiteNormClass] using hba
    have hzero : finiteNormClass A K E.field E.below (b - a) = 0 := by
      rw [finiteNormClass_sub, hba', sub_self]
    have hsub : b - a ∈ ClassFormation.FiniteGaloisSubextension.normSubgroup A E :=
      (finiteNormClass_eq_zero_iff A K E.field E.below (b - a)).1 hzero
    have hsubH : b - a ∈ H := hEH hsub
    have ha : a = b - (b - a) := by abel
    rw [ha]
    exact H.sub_mem hb hsubH
  · intro ha
    exact ⟨a, ha, rfl⟩

def

reciprocityAbelianizedSubgroup

L116 ↗

ClassFormation.FiniteGaloisSubextension.reciprocityAbelianizedSubgroup

Documentation

Transport H / N_E through a specified finite reciprocity equivalence and forget additive notation. This is a genuine subgroup of the actual abelianization G(E/K)ᵃᵇ.

The argument rE is kept explicit: this definition does not construct the finite reciprocity equivalence.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
local instance normQuotient_extensionQuotient_finite
    (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite

Lean source · statement

def reciprocityAbelianizedSubgroup
    (A : Rep ℤ G) (E : FiniteGaloisSubextension K)
    (H : AddSubgroup (ambientFixedAddSubgroup A K))
    (rE : FiniteNormQuotient A K E.field E.below ≃+
      Additive (Abelianization E.extensionQuotient)) :
    Subgroup (Abelianization E.extensionQuotient)

theorem

mem_reciprocityAbelianizedSubgroup_iff

L130 ↗

ClassFormation.FiniteGaloisSubextension.mem_reciprocityAbelianizedSubgroup_iff

Documentation

Membership in the transported subgroup is literal membership of the corresponding reciprocity class in the image of H / N_E.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
local instance normQuotient_extensionQuotient_finite
    (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite
omit [IsTopologicalGroup G] in

Lean source · statement

theorem mem_reciprocityAbelianizedSubgroup_iff
    (A : Rep ℤ G) (E : FiniteGaloisSubextension K)
    (H : AddSubgroup (ambientFixedAddSubgroup A K))
    (rE : FiniteNormQuotient A K E.field E.below ≃+
      Additive (Abelianization E.extensionQuotient))
    (q : Abelianization E.extensionQuotient) :
    q ∈ reciprocityAbelianizedSubgroup A E H rE ↔
      ∃ z ∈ normQuotientSubgroup A E H,
        rE z = Additive.ofMul q

def

reciprocityAbelianizedClassHom

L145 ↗

ClassFormation.FiniteGaloisSubextension.reciprocityAbelianizedClassHom

Documentation

The representative-level abelianized class map obtained by first passing to A_K / N_E and then applying the specified equivalence.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
local instance normQuotient_extensionQuotient_finite
    (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite

Lean source · statement

def reciprocityAbelianizedClassHom
    (A : Rep ℤ G) (E : FiniteGaloisSubextension K)
    (rE : FiniteNormQuotient A K E.field E.below ≃+
      Additive (Abelianization E.extensionQuotient)) :
    ambientFixedAddSubgroup A K →+
      Additive (Abelianization E.extensionQuotient)

theorem

reciprocityClass_mem_abelianizedSubgroup_iff

L157 ↗

ClassFormation.FiniteGaloisSubextension.reciprocityClass_mem_abelianizedSubgroup_iff

Documentation

If N_E ⊆ H, the transported subgroup has exactly H as its inverse image under the abelianized class map. This is the precise full-preimage statement used before taking the fixed field in the finite classification argument.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
local instance normQuotient_extensionQuotient_finite
    (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite
omit [IsTopologicalGroup G] in

Lean source · statement

theorem reciprocityClass_mem_abelianizedSubgroup_iff
    (A : Rep ℤ G) (E : FiniteGaloisSubextension K)
    (H : AddSubgroup (ambientFixedAddSubgroup A K))
    (hEH : ClassFormation.FiniteGaloisSubextension.normSubgroup A E ≤ H)
    (rE : FiniteNormQuotient A K E.field E.below ≃+
      Additive (Abelianization E.extensionQuotient))
    (a : ambientFixedAddSubgroup A K) :
    Additive.toMul (reciprocityAbelianizedClassHom A E rE a) ∈
        reciprocityAbelianizedSubgroup A E H rE ↔
      a ∈ H

def

abelianizationPreimageSubgroup

L186 ↗

ClassFormation.abelianizationPreimageSubgroup

Documentation

Pull a subgroup of an abelianization back to the original finite Galois group.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def abelianizationPreimageSubgroup
    {Q : Type*} [Group Q] (T : Subgroup (Abelianization Q)) :
    Subgroup Q

theorem

commutator_le_abelianizationPreimageSubgroup

L192 ↗

ClassFormation.commutator_le_abelianizationPreimageSubgroup

Documentation

Every such pullback contains the commutator subgroup.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem commutator_le_abelianizationPreimageSubgroup
    {Q : Type*} [Group Q] (T : Subgroup (Abelianization Q)) :
    commutator Q ≤ abelianizationPreimageSubgroup T

instance

candidate_extensionQuotient_finite

L208 ↗

ClassFormation.FiniteGaloisSubextension.candidate_extensionQuotient_finite

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

instance candidate_extensionQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G]
    {K : ClosedSubgroup G} (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below)

def

intermediateFiniteAbelianOfCommutatorLe

L216 ↗

ClassFormation.FiniteGaloisSubextension.intermediateFiniteAbelianOfCommutatorLe

Documentation

The actual finite abelian intermediate extension cut out by a subgroup S ≤ G(E/K) containing the commutator.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
local instance candidate_extensionQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G]
    {K : ClosedSubgroup G} (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite

Lean source · statement

def intermediateFiniteAbelianOfCommutatorLe
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {K : ClosedSubgroup G}
    (E : FiniteGaloisSubextension K)
    (S : Subgroup E.extensionQuotient)
    (hS : commutator E.extensionQuotient ≤ S) :
    FiniteAbelianSubextension K

theorem

intermediateFiniteAbelianOfCommutatorLe_field

L247 ↗

ClassFormation.FiniteGaloisSubextension.intermediateFiniteAbelianOfCommutatorLe_field

Documentation

The field underlying the preceding package is the literal fixed field of S.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
local instance candidate_extensionQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G]
    {K : ClosedSubgroup G} (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite

Lean source · statement

theorem intermediateFiniteAbelianOfCommutatorLe_field
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {K : ClosedSubgroup G}
    (E : FiniteGaloisSubextension K)
    (S : Subgroup E.extensionQuotient)
    (hS : commutator E.extensionQuotient ≤ S) :
    (intermediateFiniteAbelianOfCommutatorLe E S hS).field =
      E.intermediateField S

def

reciprocityPreimageSubgroup

L259 ↗

ClassFormation.FiniteGaloisSubextension.reciprocityPreimageSubgroup

Documentation

The subgroup obtained from H / N_E on the abelianization side, pulled back to the actual finite Galois quotient.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
local instance candidate_extensionQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G]
    {K : ClosedSubgroup G} (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite

Lean source · statement

def reciprocityPreimageSubgroup
    (A : Rep ℤ G) (E : FiniteGaloisSubextension K)
    (H : AddSubgroup (ambientFixedAddSubgroup A K))
    (rE : FiniteNormQuotient A K E.field E.below ≃+
      Additive (Abelianization E.extensionQuotient)) :
    Subgroup E.extensionQuotient

theorem

commutator_le_reciprocityPreimageSubgroup

L271 ↗

ClassFormation.FiniteGaloisSubextension.commutator_le_reciprocityPreimageSubgroup

Documentation

The actual subgroup used to define the intermediate field contains the commutator, independently of any kernel assertion for rE.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
local instance candidate_extensionQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G]
    {K : ClosedSubgroup G} (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite
omit [IsTopologicalGroup G] in

Lean source · statement

theorem commutator_le_reciprocityPreimageSubgroup
    (A : Rep ℤ G) (E : FiniteGaloisSubextension K)
    (H : AddSubgroup (ambientFixedAddSubgroup A K))
    (rE : FiniteNormQuotient A K E.field E.below ≃+
      Additive (Abelianization E.extensionQuotient)) :
    commutator E.extensionQuotient ≤
      reciprocityPreimageSubgroup A E H rE

theorem

reciprocityClass_mem_preimageSubgroup_iff

L284 ↗

ClassFormation.FiniteGaloisSubextension.reciprocityClass_mem_preimageSubgroup_iff

Documentation

The pulled-back subgroup has exactly H as the inverse image of the representative-level reciprocity class. This is the group-side form of the full-preimage assertion used in the finite-classification surjectivity proof.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
local instance candidate_extensionQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G]
    {K : ClosedSubgroup G} (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite
omit [IsTopologicalGroup G] in

Lean source · statement

theorem reciprocityClass_mem_preimageSubgroup_iff
    (A : Rep ℤ G) (E : FiniteGaloisSubextension K)
    (H : AddSubgroup (ambientFixedAddSubgroup A K))
    (hEH : ClassFormation.FiniteGaloisSubextension.normSubgroup A E ≤ H)
    (rE : FiniteNormQuotient A K E.field E.below ≃+
      Additive (Abelianization E.extensionQuotient))
    (a : ambientFixedAddSubgroup A K) :
    Quotient.out (Additive.toMul
        (reciprocityAbelianizedClassHom A E rE a)) ∈
        reciprocityPreimageSubgroup A E H rE ↔
      a ∈ H

theorem

candidateQuotient_eq_one_iff

L308 ↗

ClassFormation.FiniteGaloisSubextension.candidateQuotient_eq_one_iff

Documentation

Equivalently, the representative of the transported reciprocity class restricts trivially to the quotient cut out by the candidate precisely for the elements of H.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
open scoped commutatorElement

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
local instance candidate_extensionQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G]
    {K : ClosedSubgroup G} (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite
omit [IsTopologicalGroup G] in

Lean source · full declaration

theorem candidateQuotient_eq_one_iff
    (A : Rep ℤ G) (E : FiniteGaloisSubextension K)
    (H : AddSubgroup (ambientFixedAddSubgroup A K))
    (hEH : ClassFormation.FiniteGaloisSubextension.normSubgroup A E ≤ H)
    (rE : FiniteNormQuotient A K E.field E.below ≃+
      Additive (Abelianization E.extensionQuotient))
    (a : ambientFixedAddSubgroup A K) :
    let S := reciprocityPreimageSubgroup A E H rE
    letI : S.Normal := Subgroup.Normal.of_commutator_le E.extensionQuotient
      (commutator_le_reciprocityPreimageSubgroup A E H rE)
    QuotientGroup.mk' S
        (Quotient.out (Additive.toMul
          (reciprocityAbelianizedClassHom A E rE a))) = 1 ↔
      a ∈ H := by
  dsimp only
  let : (reciprocityPreimageSubgroup A E H rE).Normal :=
    Subgroup.Normal.of_commutator_le E.extensionQuotient
      (commutator_le_reciprocityPreimageSubgroup A E H rE)
  constructor
  · intro h
    apply (reciprocityClass_mem_preimageSubgroup_iff
      A E H hEH rE a).1
    exact (QuotientGroup.eq_one_iff _).1 h
  · intro ha
    apply (QuotientGroup.eq_one_iff _).2
    exact (reciprocityClass_mem_preimageSubgroup_iff
      A E H hEH rE a).2 ha

def