Module

FiniteAbelianSubextension.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.FiniteAbelianSubextension

33 declarations indexed from sourceView source ↗

Module documentation

Finite abelian extensions in abstract reciprocity

the finite abelian class-field classification classifies finite abelian extensions L | K by their norm subgroups. This file builds the extension side of that correspondence independently of the reciprocity isomorphism:

a finite Galois extension whose actual quotient is commutative;
the field-inclusion order (opposite to inclusion of closed subgroups);
compositum and intersection operations;
the actual assignment L ↦ N_{L/K} A_L and its unconditional order

relations.

The reverse inclusions in the two norm formulas, and hence the classification bijection itself, require the abstract reciprocity theorem and are deliberately not postulated.

Imports3

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.FiniteGaloisSubextension
Mathlib.Algebra.Group.Subgroup.Pointwise
Mathlib.Topology.Algebra.Group.Pointwise

Imported by11

structure

FiniteAbelianSubextension

L44 ↗

ClassFormation.FiniteAbelianSubextension

Documentation

A finite abelian extension L | K: a finite Galois extension together with commutativity of its actual quotient G_K/G_L.

Source context 6 commands

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

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

Lean source · full declaration

structure FiniteAbelianSubextension (K : ClosedSubgroup G) where
  /-- The underlying finite Galois subextension. -/
  toFiniteGaloisExtension : FiniteGaloisSubextension K
  /-- Commutativity of the relative Galois quotient. -/
  commutative : IsMulCommutative toFiniteGaloisExtension.extensionQuotient

abbrev

field

L55 ↗

ClassFormation.FiniteAbelianSubextension.field

Documentation

Introduces the abbreviation field.

Source context 8 commands

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

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

Lean source · statement

abbrev field (L : FiniteAbelianSubextension K) : ClosedSubgroup G

abbrev

below

L59 ↗

ClassFormation.FiniteAbelianSubextension.below

Documentation

Introduces the abbreviation below.

Source context 8 commands

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

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

Lean source · statement

abbrev below (L : FiniteAbelianSubextension K) :
    L.field.toSubgroup ≤ K.toSubgroup

abbrev

normal

L64 ↗

ClassFormation.FiniteAbelianSubextension.normal

Documentation

Introduces the abbreviation normal.

Source context 8 commands

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

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

Lean source · statement

abbrev normal (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal

abbrev

finite

L69 ↗

ClassFormation.FiniteAbelianSubextension.finite

Documentation

Introduces the abbreviation finite.

Source context 8 commands

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

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

Lean source · statement

abbrev finite (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below)

def

extensionQuotient

L77 ↗

ClassFormation.FiniteAbelianSubextension.extensionQuotient

Documentation

The finite abelian quotient carried by the extension. Its representation is inherited through the finite Galois extension boundary rather than exposed as a transparent quotient abbreviation.

Source context 8 commands

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

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

Lean source · statement

def extensionQuotient (L : FiniteAbelianSubextension K) : Type u

instance

extensionQuotient_commGroup

L82 ↗

ClassFormation.FiniteAbelianSubextension.extensionQuotient_commGroup

Documentation

The quotient attached to a finite abelian subextension is a commutative group.

Source context 8 commands

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

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

Lean source · statement

instance extensionQuotient_commGroup (L : FiniteAbelianSubextension K) :
    CommGroup L.extensionQuotient

instance

extensionQuotient_finite

L93 ↗

ClassFormation.FiniteAbelianSubextension.extensionQuotient_finite

Documentation

The quotient attached to a finite abelian subextension is finite.

Source context 8 commands

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

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

Lean source · statement

instance extensionQuotient_finite (L : FiniteAbelianSubextension K) :
    Finite L.extensionQuotient

def

extensionQuotientMulEquiv

L100 ↗

ClassFormation.FiniteAbelianSubextension.extensionQuotientMulEquiv

Documentation

Comparison with the quotient presentation used by the underlying group library.

Source context 8 commands

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

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

Lean source · statement

def extensionQuotientMulEquiv (L : FiniteAbelianSubextension K) :
    L.extensionQuotient ≃*
      (K.toSubgroup ⧸ extensionSubgroup K L.field L.below)

def

extensionQuotientMk

L106 ↗

ClassFormation.FiniteAbelianSubextension.extensionQuotientMk

Documentation

The canonical quotient projection for a finite abelian extension.

Source context 8 commands

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

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

Lean source · statement

def extensionQuotientMk (L : FiniteAbelianSubextension K) :
    K.toSubgroup →* L.extensionQuotient

theorem

extensionQuotientMk_apply

L112 ↗

ClassFormation.FiniteAbelianSubextension.extensionQuotientMk_apply

Documentation

The named abelian quotient projection agrees with the underlying quotient map.

Source context 8 commands

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

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

Lean source · statement

theorem extensionQuotientMk_apply (L : FiniteAbelianSubextension K)
    (k : K.toSubgroup) :
    L.extensionQuotientMulEquiv (L.extensionQuotientMk k) =
      (QuotientGroup.mk k :
        K.toSubgroup ⧸ extensionSubgroup K L.field L.below)

theorem

extensionQuotient_inductionOn

L120 ↗

ClassFormation.FiniteAbelianSubextension.extensionQuotient_inductionOn

Documentation

Eliminate an abelian extension quotient without choosing a representative.

Source context 8 commands

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

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

Lean source · statement

theorem extensionQuotient_inductionOn
    (L : FiniteAbelianSubextension K)
    {motive : L.extensionQuotient → Prop} (q : L.extensionQuotient)
    (mk : ∀ k : K.toSubgroup, motive (L.extensionQuotientMk k)) :
    motive q

theorem

ext

L130 ↗

ClassFormation.FiniteAbelianSubextension.ext

Documentation

Two packages with the same closed subgroup represent the same finite abelian extension.

Source context 8 commands

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

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

Lean source · statement

theorem ext {L₁ L₂ : FiniteAbelianSubextension K}
    (h : L₁.field = L₂.field) : L₁ = L₂

instance

(anonymous instance)

L146 ↗

Documentation

The order is field inclusion. Since fields are represented by their absolute Galois subgroups, it is the opposite subgroup order.

Source context 8 commands

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

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

Lean source · full declaration

instance : PartialOrder (FiniteAbelianSubextension K) where
  le L₁ L₂ := L₂.field.toSubgroup ≤ L₁.field.toSubgroup
  le_refl _ := le_rfl
  le_trans _ _ _ h₁₂ h₂₃ := h₂₃.trans h₁₂
  le_antisymm L₁ L₂ h₁₂ h₂₁ := by
    apply ext
    apply ClosedSubgroup.ext
    have hs : L₁.field.toSubgroup = L₂.field.toSubgroup :=
      le_antisymm h₂₁ h₁₂
    exact congrArg (fun H : Subgroup G => H.carrier) hs

theorem

le_iff

L158 ↗

ClassFormation.FiniteAbelianSubextension.le_iff

Documentation

The order on finite abelian subextensions is characterized by containment of their fields.

Source context 8 commands

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

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

Lean source · statement

theorem le_iff (L₁ L₂ : FiniteAbelianSubextension K) :
    L₁ ≤ L₂ ↔ L₂.field.toSubgroup ≤ L₁.field.toSubgroup

def

baseChange

L165 ↗

ClassFormation.FiniteAbelianSubextension.baseChange

Documentation

Base change of a finite abelian extension to an arbitrary intermediate abstract field. Contravariantly the new top subgroup is the intersection with the new base subgroup.

Source context 8 commands

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

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

Lean source · full declaration

def baseChange (M : FiniteAbelianSubextension K)
    (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) :
    FiniteAbelianSubextension L where
  toFiniteGaloisExtension :=
    M.toFiniteGaloisExtension.baseChange L hLK
  commutative := by
    let P :=
      M.toFiniteGaloisExtension.baseChange L hLK
    let :
        (extensionSubgroup K M.field M.below).Normal :=
      M.normal
    let :
        (extensionSubgroup L P.field P.below).Normal :=
      P.normal
    refine ⟨⟨?_⟩⟩
    intro x y
    refine P.extensionQuotient_inductionOn
      (motive := fun x => x * y = y * x) x ?_
    intro a
    refine P.extensionQuotient_inductionOn
      (motive := fun y =>
        P.extensionQuotientMk a * y =
          y * P.extensionQuotientMk a) y ?_
    intro b
    apply P.extensionQuotientMulEquiv.injective
    simp only [map_mul, P.extensionQuotientMk_apply]
    apply QuotientGroup.eq.mpr
    apply (mem_extensionSubgroup_iff L P.field P.below _).2
    constructor
    · exact ((a * b)⁻¹ * (b * a)).property
    · let aK : K.toSubgroup :=
        Subgroup.inclusion hLK a
      let bK : K.toSubgroup :=
        Subgroup.inclusion hLK b
      have hcomm :=
        M.commutative.is_comm.comm
          (M.extensionQuotientMk aK)
          (M.extensionQuotientMk bK)
      have hcommRaw :=
        congrArg M.extensionQuotientMulEquiv hcomm
      simp only [map_mul, M.extensionQuotientMk_apply] at hcommRaw
      exact
        (mem_extensionSubgroup_iff
          K M.field M.below _).1
          (QuotientGroup.eq.mp hcommRaw)

def

compositum

L214 ↗

ClassFormation.FiniteAbelianSubextension.compositum

Documentation

The compositum L₁L₂, contravariantly represented by G_{L₁} ∩ G_{L₂}.

Source context 8 commands

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

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

Lean source · full declaration

def compositum (L₁ L₂ : FiniteAbelianSubextension K) :
    FiniteAbelianSubextension K where
  toFiniteGaloisExtension :=
    L₁.toFiniteGaloisExtension.compositum L₂.toFiniteGaloisExtension
  commutative := by
    let P := L₁.toFiniteGaloisExtension.compositum
      L₂.toFiniteGaloisExtension
    let : (extensionSubgroup K L₁.field L₁.below).Normal := L₁.normal
    let : (extensionSubgroup K L₂.field L₂.below).Normal := L₂.normal
    let : (extensionSubgroup K P.field P.below).Normal := P.normal
    refine ⟨⟨?_⟩⟩
    intro x y
    refine P.extensionQuotient_inductionOn
      (motive := fun x => x * y = y * x) x ?_
    intro a
    refine P.extensionQuotient_inductionOn
      (motive := fun y => P.extensionQuotientMk a * y =
        y * P.extensionQuotientMk a) y ?_
    intro b
    apply P.extensionQuotientMulEquiv.injective
    simp only [map_mul, P.extensionQuotientMk_apply]
    apply QuotientGroup.eq.mpr
    apply (mem_extensionSubgroup_iff K P.field P.below _).2
    constructor
    · have hcomm := L₁.commutative.is_comm.comm
          (L₁.extensionQuotientMk a) (L₁.extensionQuotientMk b)
      have hcommRaw := congrArg L₁.extensionQuotientMulEquiv hcomm
      simp only [map_mul, L₁.extensionQuotientMk_apply] at hcommRaw
      exact (mem_extensionSubgroup_iff K L₁.field L₁.below _).1
        (QuotientGroup.eq.mp hcommRaw)
    · have hcomm := L₂.commutative.is_comm.comm
          (L₂.extensionQuotientMk a) (L₂.extensionQuotientMk b)
      have hcommRaw := congrArg L₂.extensionQuotientMulEquiv hcomm
      simp only [map_mul, L₂.extensionQuotientMk_apply] at hcommRaw
      exact (mem_extensionSubgroup_iff K L₂.field L₂.below _).1
        (QuotientGroup.eq.mp hcommRaw)

theorem

le_compositum_left

L252 ↗

ClassFormation.FiniteAbelianSubextension.le_compositum_left

Documentation

The left subextension embeds into the compositum.

Source context 8 commands

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

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

Lean source · statement

theorem le_compositum_left (L₁ L₂ : FiniteAbelianSubextension K) :
    L₁ ≤ L₁.compositum L₂

theorem

le_compositum_right

L260 ↗

ClassFormation.FiniteAbelianSubextension.le_compositum_right

Documentation

The right subextension embeds into the compositum.

Source context 8 commands

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

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

Lean source · statement

theorem le_compositum_right (L₁ L₂ : FiniteAbelianSubextension K) :
    L₂ ≤ L₁.compositum L₂

theorem

compositum_le

L268 ↗

ClassFormation.FiniteAbelianSubextension.compositum_le

Documentation

The compositum is the least subextension containing both inputs.

Source context 8 commands

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

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

Lean source · statement

theorem compositum_le {L₁ L₂ P : FiniteAbelianSubextension K}
    (h₁ : L₁ ≤ P) (h₂ : L₂ ≤ P) :
    L₁.compositum L₂ ≤ P

theorem

field_le_normalizer

L281 ↗

ClassFormation.FiniteAbelianSubextension.field_le_normalizer

Documentation

Each field subgroup normalizes the other one. This is not an ambient-normality assumption: it is obtained from the packaged normality of G_L inside G_K.

Source context 11 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {K : ClosedSubgroup G}
section Intersection
variable [IsTopologicalGroup G] [CompactSpace G]
omit [IsTopologicalGroup G] [CompactSpace G] in

Lean source · statement

theorem field_le_normalizer (L₁ L₂ : FiniteAbelianSubextension K) :
    L₁.field.toSubgroup ≤ Subgroup.normalizer L₂.field.toSubgroup

def

intersectionField

L293 ↗

ClassFormation.FiniteAbelianSubextension.intersectionField

Documentation

The field intersection L₁ ∩ L₂, contravariantly represented by the subgroup generated by G_{L₁} and G_{L₂}. Its closedness follows from the product description and compactness.

Source context 10 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {K : ClosedSubgroup G}
section Intersection
variable [IsTopologicalGroup G] [CompactSpace G]

Lean source · full declaration

def intersectionField (L₁ L₂ : FiniteAbelianSubextension K) :
    ClosedSubgroup G where
  toSubgroup := L₁.field.toSubgroup ⊔ L₂.field.toSubgroup
  isClosed' := by
    change IsClosed
      ((↑(L₁.field.toSubgroup ⊔ L₂.field.toSubgroup) : Set G))
    rw [Subgroup.coe_mul_of_left_le_normalizer_right _ _
      (field_le_normalizer L₁ L₂)]
    exact L₂.field.isClosed'.mul_left_of_isCompact
      L₁.field.isClosed'.isCompact

theorem

intersectionField_below

L305 ↗

ClassFormation.FiniteAbelianSubextension.intersectionField_below

Documentation

The intersection field remains above the fixed base field.

Source context 10 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {K : ClosedSubgroup G}
section Intersection
variable [IsTopologicalGroup G] [CompactSpace G]

Lean source · statement

theorem intersectionField_below (L₁ L₂ : FiniteAbelianSubextension K) :
    (intersectionField L₁ L₂).toSubgroup ≤ K.toSubgroup

theorem

extensionSubgroup_intersectionField

L311 ↗

ClassFormation.FiniteAbelianSubextension.extensionSubgroup_intersectionField

Documentation

Viewing the generated ambient subgroup inside G_K agrees with taking the supremum of the two actual extension subgroups.

Source context 10 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {K : ClosedSubgroup G}
section Intersection
variable [IsTopologicalGroup G] [CompactSpace G]

Lean source · statement

theorem extensionSubgroup_intersectionField (L₁ L₂ :
    FiniteAbelianSubextension K) :
    extensionSubgroup K (intersectionField L₁ L₂)
        (intersectionField_below L₁ L₂) =
      extensionSubgroup K L₁.field L₁.below ⊔
        extensionSubgroup K L₂.field L₂.below

def

intersectionGalois

L321 ↗

ClassFormation.FiniteAbelianSubextension.intersectionGalois

Documentation

The finite Galois package underlying the intersection field.

Source context 10 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {K : ClosedSubgroup G}
section Intersection
variable [IsTopologicalGroup G] [CompactSpace G]

Lean source · full declaration

def intersectionGalois (L₁ L₂ : FiniteAbelianSubextension K) :
    FiniteGaloisSubextension K where
  field := intersectionField L₁ L₂
  below := intersectionField_below L₁ L₂
  normal := by
    rw [extensionSubgroup_intersectionField]
    let : (extensionSubgroup K L₁.field L₁.below).Normal := L₁.normal
    let : (extensionSubgroup K L₂.field L₂.below).Normal := L₂.normal
    exact Subgroup.sup_normal _ _
  finite := by
    rw [extensionSubgroup_intersectionField]
    let : (extensionSubgroup K L₁.field L₁.below).FiniteIndex :=
      @Subgroup.finiteIndex_of_finite_quotient K.toSubgroup _
        (extensionSubgroup K L₁.field L₁.below) L₁.finite
    let : (extensionSubgroup K L₁.field L₁.below ⊔
        extensionSubgroup K L₂.field L₂.below).FiniteIndex :=
      Subgroup.finiteIndex_of_le le_sup_left
    exact Subgroup.finite_quotient_of_finiteIndex

def

intersection

L341 ↗

ClassFormation.FiniteAbelianSubextension.intersection

Documentation

The intersection of two finite abelian extensions.

Source context 10 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {K : ClosedSubgroup G}
section Intersection
variable [IsTopologicalGroup G] [CompactSpace G]

Lean source · full declaration

def intersection (L₁ L₂ : FiniteAbelianSubextension K) :
    FiniteAbelianSubextension K where
  toFiniteGaloisExtension := intersectionGalois L₁ L₂
  commutative := by
    let P := intersectionGalois L₁ L₂
    let : (extensionSubgroup K L₁.field L₁.below).Normal := L₁.normal
    let : (extensionSubgroup K L₂.field L₂.below).Normal := L₂.normal
    let : (extensionSubgroup K P.field P.below).Normal := P.normal
    refine ⟨⟨?_⟩⟩
    intro x y
    refine P.extensionQuotient_inductionOn
      (motive := fun x => x * y = y * x) x ?_
    intro a
    refine P.extensionQuotient_inductionOn
      (motive := fun y => P.extensionQuotientMk a * y =
        y * P.extensionQuotientMk a) y ?_
    intro b
    apply P.extensionQuotientMulEquiv.injective
    simp only [map_mul, P.extensionQuotientMk_apply]
    apply QuotientGroup.eq.mpr
    change (a * b)⁻¹ * (b * a) ∈
      extensionSubgroup K (intersectionField L₁ L₂)
        (intersectionField_below L₁ L₂)
    rw [extensionSubgroup_intersectionField]
    have hcomm := L₁.commutative.is_comm.comm
      (L₁.extensionQuotientMk a) (L₁.extensionQuotientMk b)
    have hcommRaw := congrArg L₁.extensionQuotientMulEquiv hcomm
    simp only [map_mul, L₁.extensionQuotientMk_apply] at hcommRaw
    have hin : (a * b)⁻¹ * (b * a) ∈
        extensionSubgroup K L₁.field L₁.below :=
      QuotientGroup.eq.mp hcommRaw
    exact (show extensionSubgroup K L₁.field L₁.below ≤
      extensionSubgroup K L₁.field L₁.below ⊔
        extensionSubgroup K L₂.field L₂.below from le_sup_left) hin

theorem

intersection_le_left

L377 ↗

ClassFormation.FiniteAbelianSubextension.intersection_le_left

Documentation

The intersection subextension lies below its left input.

Source context 10 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {K : ClosedSubgroup G}
section Intersection
variable [IsTopologicalGroup G] [CompactSpace G]

Lean source · statement

theorem intersection_le_left (L₁ L₂ : FiniteAbelianSubextension K) :
    L₁.intersection L₂ ≤ L₁

theorem

intersection_le_right

L384 ↗

ClassFormation.FiniteAbelianSubextension.intersection_le_right

Documentation

The intersection subextension lies below its right input.

Source context 10 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {K : ClosedSubgroup G}
section Intersection
variable [IsTopologicalGroup G] [CompactSpace G]

Lean source · statement

theorem intersection_le_right (L₁ L₂ : FiniteAbelianSubextension K) :
    L₁.intersection L₂ ≤ L₂

theorem

le_intersection

L391 ↗

ClassFormation.FiniteAbelianSubextension.le_intersection

Documentation

A subextension below both inputs lies below their intersection.

Source context 10 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {K : ClosedSubgroup G}
section Intersection
variable [IsTopologicalGroup G] [CompactSpace G]

Lean source · statement

theorem le_intersection {P L₁ L₂ : FiniteAbelianSubextension K}
    (h₁ : P ≤ L₁) (h₂ : P ≤ L₂) :
    P ≤ L₁.intersection L₂

def

normSubgroup

L415 ↗

ClassFormation.FiniteAbelianSubextension.normSubgroup

Documentation

The norm subgroup assigned to a finite abelian extension, N_L = N_{L/K} A_L in the finite abelian class-field classification.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
universe u
section Representation

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

Lean source · statement

def normSubgroup (A : Rep ℤ G) (L : FiniteAbelianSubextension K) :
    AddSubgroup (ambientFixedAddSubgroup A K)

theorem

normSubgroup_antitone

L423 ↗

ClassFormation.FiniteAbelianSubextension.normSubgroup_antitone

Documentation

The source-level implication in the order formula: an inclusion of fields gives the reverse inclusion of norm subgroups.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
universe u
section Representation

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

Lean source · statement

theorem normSubgroup_antitone (A : Rep ℤ G)
    {L₁ L₂ : FiniteAbelianSubextension K} (h : L₁ ≤ L₂) :
    normSubgroup A L₂ ≤ normSubgroup A L₁

theorem

normSubgroup_compositum_le_inf

L453 ↗

ClassFormation.FiniteAbelianSubextension.normSubgroup_compositum_le_inf

Documentation

The unconditional half of N_{L₁L₂} = N_{L₁} ∩ N_{L₂} in the finite abelian class-field classification.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
universe u
section Representation

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

Lean source · statement

theorem normSubgroup_compositum_le_inf (A : Rep ℤ G)
    (L₁ L₂ : FiniteAbelianSubextension K) :
    normSubgroup A (L₁.compositum L₂) ≤
      normSubgroup A L₁ ⊓ normSubgroup A L₂

theorem

sup_normSubgroup_le_intersection

L463 ↗

ClassFormation.FiniteAbelianSubextension.sup_normSubgroup_le_intersection

Documentation

The unconditional half of N_{L₁∩L₂} = N_{L₁}N_{L₂} in additive notation.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory
universe u
section Representation

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

Lean source · statement

theorem sup_normSubgroup_le_intersection
    [IsTopologicalGroup G] [CompactSpace G]
    (A : Rep ℤ G) (L₁ L₂ : FiniteAbelianSubextension K) :
    normSubgroup A L₁ ⊔ normSubgroup A L₂ ≤
      normSubgroup A (L₁.intersection L₂)

Module documentation

Finite abelian extensions in abstract reciprocity

Declarations