Module

NormConjugation.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.NormConjugation

12 declarations indexed from sourceView source ↗

Module documentation

Conjugation and relative norms

These are the field-conjugation and norm identities used in the abstract reciprocity construction and theorem. They belong before the reciprocity construction: their proofs use only the actual relative norm and the conjugation action.

Imports2

Imported by3

theorem

conjugateClosedSubgroup_mono

L37 ↗

ClassFormation.conjugateClosedSubgroup_mono

Documentation

Conjugation preserves inclusions of abstract fields.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem conjugateClosedSubgroup_mono [ContinuousMul G]
    {K L : ClosedSubgroup G} (hLK : L.toSubgroup ≤ K.toSubgroup)
    (s : G) :
    (conjugateClosedSubgroup L s).toSubgroup ≤
      (conjugateClosedSubgroup K s).toSubgroup

def

conjugateSubgroupEquiv

L50 ↗

ClassFormation.conjugateSubgroupEquiv

Documentation

Conjugation by s⁻¹ identifies a field subgroup with the subgroup representing its right conjugate K^s.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · full declaration

def conjugateSubgroupEquiv [ContinuousMul G]
    (K : ClosedSubgroup G) (s : G) :
    K.toSubgroup ≃* (conjugateClosedSubgroup K s).toSubgroup where
  toFun k := ⟨s⁻¹ * k.1 * s, by
    change s⁻¹ * k.1 * s ∈ conjugateClosedSubgroup K s
    rw [conjugateClosedSubgroup_mem]
    convert k.2 using 1
    simp [mul_assoc]⟩
  invFun x := ⟨s * x.1 * s⁻¹,
    (conjugateClosedSubgroup_mem K s x.1).mp x.2⟩
  left_inv k := by
    apply Subtype.ext
    simp [mul_assoc]
  right_inv x := by
    apply Subtype.ext
    simp [mul_assoc]
  map_mul' a b := by
    apply Subtype.ext
    simp [mul_assoc]

theorem

conjugateSubgroupEquiv_apply_coe

L72 ↗

ClassFormation.conjugateSubgroupEquiv_apply_coe

Documentation

Establishes the identity (conjugateSubgroupEquiv K s k).1 = s⁻¹ * k.1 * s.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem conjugateSubgroupEquiv_apply_coe [ContinuousMul G]
    (K : ClosedSubgroup G) (s : G) (k : K.toSubgroup) :
    (conjugateSubgroupEquiv K s k).1 = s⁻¹ * k.1 * s

theorem

map_extensionSubgroup_conjugate

L79 ↗

ClassFormation.map_extensionSubgroup_conjugate

Documentation

Conjugation carries the subgroup for L/K exactly to the subgroup for L^s/K^s.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem map_extensionSubgroup_conjugate [ContinuousMul G]
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G) :
    (extensionSubgroup K L hLK).map
        (conjugateSubgroupEquiv K s).toMonoidHom =
      extensionSubgroup (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)

def

relativeConjugateCosetEquiv

L101 ↗

ClassFormation.relativeConjugateCosetEquiv

Documentation

Conjugation identifies the relative coset spaces even when the extension is not normal.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def relativeConjugateCosetEquiv [ContinuousMul G]
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G) :
    (K.toSubgroup ⧸ extensionSubgroup K L hLK) ≃
      ((conjugateClosedSubgroup K s).toSubgroup ⧸
        extensionSubgroup (conjugateClosedSubgroup K s)
          (conjugateClosedSubgroup L s)
          (conjugateClosedSubgroup_mono hLK s))

theorem

relativeConjugateCosetEquiv_mk

L136 ↗

ClassFormation.relativeConjugateCosetEquiv_mk

Documentation

Establishes the identity relativeConjugateCosetEquiv K L hLK s (QuotientGroup.mk k) = QuotientGroup.mk (conjugateSubgroupEquiv K s k).

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem relativeConjugateCosetEquiv_mk [ContinuousMul G]
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G)
    (k : K.toSubgroup) :
    relativeConjugateCosetEquiv K L hLK s (QuotientGroup.mk k) =
      QuotientGroup.mk (conjugateSubgroupEquiv K s k)

instance

conjugateExtension_normal

L145 ↗

ClassFormation.conjugateExtension_normal

Documentation

A conjugate of a Galois extension is Galois.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

instance conjugateExtension_normal [ContinuousMul G]
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K L hLK).Normal] :
    (extensionSubgroup (conjugateClosedSubgroup K s)
      (conjugateClosedSubgroup L s)
      (conjugateClosedSubgroup_mono hLK s)).Normal

def

finiteReciprocityNaturalityConjugation

L159 ↗

ClassFormation.finiteReciprocityNaturalityConjugation

Documentation

The left vertical isomorphism in the conjugation diagram of norm--conjugation naturality, τ ↦ s⁻¹τs.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def finiteReciprocityNaturalityConjugation
    [ContinuousMul G] (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K L hLK).Normal] :
    (K.toSubgroup ⧸ extensionSubgroup K L hLK) ≃*
      ((conjugateClosedSubgroup K s).toSubgroup ⧸
        extensionSubgroup (conjugateClosedSubgroup K s)
          (conjugateClosedSubgroup L s)
          (conjugateClosedSubgroup_mono hLK s))

theorem

finiteReciprocityNaturalityConjugation_mk

L181 ↗

ClassFormation.finiteReciprocityNaturalityConjugation_mk

Documentation

Establishes the identity finiteReciprocityNaturalityConjugation K L hLK s (QuotientGroup.mk k) = QuotientGroup.mk (conjugateSubgroupEquiv K s k).

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem finiteReciprocityNaturalityConjugation_mk [ContinuousMul G]
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    (k : K.toSubgroup) :
    finiteReciprocityNaturalityConjugation K L hLK s (QuotientGroup.mk k) =
      QuotientGroup.mk (conjugateSubgroupEquiv K s k)

theorem

finite_conjugateExtension

L191 ↗

ClassFormation.finite_conjugateExtension

Documentation

Conjugation preserves finiteness of the Galois quotient.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem finite_conjugateExtension [ContinuousMul G]
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G)
    [hLfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)] :
    Finite ((conjugateClosedSubgroup K s).toSubgroup ⧸
      extensionSubgroup (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s))

theorem

relativeCosetAction_conjugate

L212 ↗

ClassFormation.relativeCosetAction_conjugate

Documentation

Conjugation intertwines the two relative coset actions.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
universe u
section Representation

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

Lean source · statement

theorem relativeCosetAction_conjugate
    [ContinuousMul G] (A : Rep ℤ G)
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G)
    (a : ambientFixedAddSubgroup A L)
    (q : K.toSubgroup ⧸ extensionSubgroup K L hLK) :
    relativeCosetAction A (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)
        (conjugateFixedElement A L s a)
        (relativeConjugateCosetEquiv K L hLK s q) =
      A.ρ s⁻¹ (relativeCosetAction A K L hLK a q)

theorem

relativeNorm_conjugate_apply

L243 ↗

ClassFormation.relativeNorm_conjugate_apply

Documentation

Relative norms commute with the right conjugation used in the second diagram of norm--conjugation naturality: N_{L^s/K^s}(a^s) = N_{L/K}(a)^s.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
universe u
section Representation

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

Lean source · full declaration

theorem relativeNorm_conjugate_apply
    [ContinuousMul G] (A : Rep ℤ G)
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G)
    [hLfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (a : ambientFixedAddSubgroup A L) :
    letI : Finite ((conjugateClosedSubgroup K s).toSubgroup ⧸
        extensionSubgroup (conjugateClosedSubgroup K s)
          (conjugateClosedSubgroup L s)
          (conjugateClosedSubgroup_mono hLK s)) :=
      finite_conjugateExtension K L hLK s
    relativeNorm A (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)
        (conjugateFixedElement A L s a) =
      conjugateFixedElement A K s (relativeNorm A K L hLK a) := by
  let hConj := conjugateClosedSubgroup_mono hLK s
  let := Fintype.ofFinite
    (K.toSubgroup ⧸ extensionSubgroup K L hLK)
  let e := relativeConjugateCosetEquiv K L hLK s
  let conjugateFintype : Fintype
      ((conjugateClosedSubgroup K s).toSubgroup ⧸
        extensionSubgroup (conjugateClosedSubgroup K s)
          (conjugateClosedSubgroup L s) hConj) :=
    Fintype.ofEquiv (K.toSubgroup ⧸ extensionSubgroup K L hLK) e
  have hconjugateFintype : Fintype.ofFinite
      ((conjugateClosedSubgroup K s).toSubgroup ⧸
        extensionSubgroup (conjugateClosedSubgroup K s)
          (conjugateClosedSubgroup L s) hConj) = conjugateFintype :=
    Subsingleton.elim _ _
  apply Subtype.ext
  simp only [relativeNorm_apply_coe, relativeNormValue,
    conjugateFixedElement_coe]
  rw [hconjugateFintype]
  calc
    ∑ q, relativeCosetAction A (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s) hConj
        (conjugateFixedElement A L s a) q =
      ∑ q, relativeCosetAction A (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s) hConj
        (conjugateFixedElement A L s a) (e q) := by
          exact (e.sum_comp fun q =>
            relativeCosetAction A (conjugateClosedSubgroup K s)
              (conjugateClosedSubgroup L s) hConj
              (conjugateFixedElement A L s a) q).symm
    _ = ∑ q, A.ρ s⁻¹ (relativeCosetAction A K L hLK a q) := by
      apply Finset.sum_congr rfl
      intro q _
      exact relativeCosetAction_conjugate A K L hLK s a q
    _ = A.ρ s⁻¹ (∑ q, relativeCosetAction A K L hLK a q) := by
      rw [map_sum]

Module documentation

Conjugation and relative norms

Declarations