NYLL
Module

FiniteAbelianClassification.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.FiniteAbelianClassification
36 declarations indexed from sourceView source ↗

Module documentation

Finite abelian classification by norm subgroups

The first paragraph of the finite classification proof uses the two restriction maps from the Galois group of a compositum. This file constructs those maps on the actual finite quotients and proves that they are jointly injective. This is the group-theoretic source of the implication that a reciprocity class which restricts trivially to both subextensions is already trivial on their compositum.

Recovering a field from the order of its finite quotient

Imports2
Imported by8

Declarations

instance

extensionQuotient_normal

L36 ↗
ClassFormation.FiniteAbelianSubextension.extensionQuotient_normal
Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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
instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal
instance

representedQuotient_finite

L42 ↗
ClassFormation.FiniteAbelianSubextension.representedQuotient_finite
Source context 7 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
Lean source · statement
instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below)
def

NormOpenAddSubgroup

L51 ↗
ClassFormation.FiniteAbelianSubextension.NormOpenAddSubgroup
Documentation

Additive subgroups which are open for the explicitly declared norm topology. The topology is part of the predicate, so no ambient topology instance is changed outside the finite abelian classification theorem.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
def NormOpenAddSubgroup (A : Rep ℤ G) (K : ClosedSubgroup G)
instance

normOpenAddSubgroupPartialOrder

L58 ↗
ClassFormation.FiniteAbelianSubextension.normOpenAddSubgroupPartialOrder
Documentation

Norm-open subgroups inherit the literal inclusion order of their underlying additive subgroups. This instance is stated explicitly because NormOpenAddSubgroup is an opaque boundary type, not a transparent alias.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
instance normOpenAddSubgroupPartialOrder (A : Rep ℤ G)
    (K : ClosedSubgroup G) : PartialOrder (NormOpenAddSubgroup A K)
def

normSubgroupMap

L64 ↗
ClassFormation.FiniteAbelianSubextension.normSubgroupMap
Documentation

The actual map in the finite abelian classification theorem, L ↦ N_{L/K} A_L, with openness carried by the codomain rather than assumed.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
def normSubgroupMap (A : Rep ℤ G)
    (L : FiniteAbelianSubextension K) : NormOpenAddSubgroup A K
theorem

normSubgroupMap_val

L74 ↗
ClassFormation.FiniteAbelianSubextension.normSubgroupMap_val
Documentation

Establishes the identity (L.normSubgroupMap A).1 = L.normSubgroup A.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
theorem normSubgroupMap_val
    (A : Rep ℤ G) (L : FiniteAbelianSubextension K) :
    (L.normSubgroupMap A).1 = L.normSubgroup A
theorem

sup_normSubgroup_isOpen

L82 ↗
ClassFormation.FiniteAbelianSubextension.sup_normSubgroup_isOpen
Documentation

The subgroup product N_{L₁}N_{L₂} (a supremum in additive notation) is open in the norm topology. It contains the defining norm neighbourhood attached to L₁.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
theorem sup_normSubgroup_isOpen (A : Rep ℤ G)
    (L₁ L₂ : FiniteAbelianSubextension K) :
    IsNormOpen A K
      ((L₁.normSubgroup A ⊔ L₂.normSubgroup A :
        AddSubgroup (ambientFixedAddSubgroup A K)) :
        Set (ambientFixedAddSubgroup A K))
theorem

normSubgroup_compositum_eq_inf_of_reciprocity_bijective

L98 ↗
ClassFormation.FiniteAbelianSubextension.normSubgroup_compositum_eq_inf_of_reciprocity_bijective
Documentation

The finite classification compositum argument, isolated as a private diagram chase. The final public theorem supplies the three bijectivity facts directly from finite reciprocity; they are not exposed as hypotheses of the classification.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
theorem normSubgroup_compositum_eq_inf_of_reciprocity_bijective
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (D : DegreeData G) (A : Rep ℤ G) (v : ValuationData D A)
    (hAxiom : v.SatisfiesUnramifiedUnitCohomology D)
    (K : FiniteAbstractField G)
    (L₁ L₂ : FiniteAbelianSubextension K.field)
    (hbij₁ : Function.Bijective
      (D.finiteReciprocityHom A v hAxiom K L₁.field L₁.below))
    (hbij₂ : Function.Bijective
      (D.finiteReciprocityHom A v hAxiom K L₂.field L₂.below))
    (hbijP : Function.Bijective
      (D.finiteReciprocityHom A v hAxiom K (L₁.compositum L₂).field
        (L₁.compositum L₂).below)) :
    (L₁.compositum L₂).normSubgroup A =
      L₁.normSubgroup A ⊓ L₂.normSubgroup A
def

restriction

L238 ↗
ClassFormation.FiniteAbelianSubextension.restriction
Documentation

Restriction along an inclusion of finite abelian subextensions. The proof-dependent raw quotient map is transported through the two named quotient boundaries here and nowhere in its callers.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
def restriction
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    {L₁ L₂ : FiniteAbelianSubextension K} (h₁₂ : L₁ ≤ L₂) :
    L₂.extensionQuotient →* L₁.extensionQuotient
theorem

restriction_mk

L252 ↗
ClassFormation.FiniteAbelianSubextension.restriction_mk
Documentation

Establishes the identity restriction h₁₂ (L₂.extensionQuotientMk k) = L₁.extensionQuotientMk k.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
theorem restriction_mk
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    {L₁ L₂ : FiniteAbelianSubextension K} (h₁₂ : L₁ ≤ L₂)
    (k : K.toSubgroup) :
    restriction h₁₂ (L₂.extensionQuotientMk k) =
      L₁.extensionQuotientMk k
def

compositumRestrictionLeft

L263 ↗
ClassFormation.FiniteAbelianSubextension.compositumRestrictionLeft
Documentation

Restriction from the actual Galois quotient of L₁L₂ / K to that of L₁ / K.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
def compositumRestrictionLeft
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L₁ L₂ : FiniteAbelianSubextension K) :
    (L₁.compositum L₂).extensionQuotient →* L₁.extensionQuotient
def

compositumRestrictionRight

L271 ↗
ClassFormation.FiniteAbelianSubextension.compositumRestrictionRight
Documentation

Restriction from the actual Galois quotient of L₁L₂ / K to that of L₂ / K.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
def compositumRestrictionRight
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L₁ L₂ : FiniteAbelianSubextension K) :
    (L₁.compositum L₂).extensionQuotient →* L₂.extensionQuotient
theorem

compositumRestrictionLeft_mk

L282 ↗
ClassFormation.FiniteAbelianSubextension.compositumRestrictionLeft_mk
Documentation

Establishes the identity compositumRestrictionLeft L₁ L₂ ((L₁.compositum L₂).extensionQuotientMk k) = L₁.extensionQuotientMk k.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
theorem compositumRestrictionLeft_mk
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L₁ L₂ : FiniteAbelianSubextension K) (k : K.toSubgroup) :
    compositumRestrictionLeft L₁ L₂
        ((L₁.compositum L₂).extensionQuotientMk k) =
      L₁.extensionQuotientMk k
theorem

compositumRestrictionRight_mk

L295 ↗
ClassFormation.FiniteAbelianSubextension.compositumRestrictionRight_mk
Documentation

Establishes the identity compositumRestrictionRight L₁ L₂ ((L₁.compositum L₂).extensionQuotientMk k) = L₂.extensionQuotientMk k.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
theorem compositumRestrictionRight_mk
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L₁ L₂ : FiniteAbelianSubextension K) (k : K.toSubgroup) :
    compositumRestrictionRight L₁ L₂
        ((L₁.compositum L₂).extensionQuotientMk k) =
      L₂.extensionQuotientMk k
theorem

compositumRestriction_joint_injective

L307 ↗
ClassFormation.FiniteAbelianSubextension.compositumRestriction_joint_injective
Documentation

The two restriction maps from the Galois group of a compositum are jointly injective. This is proved on the literal quotient representatives: an element trivial modulo both field subgroups lies in their intersection, which is the subgroup representing the compositum.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · full declaration
theorem compositumRestriction_joint_injective
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L₁ L₂ : FiniteAbelianSubextension K) :
    Function.Injective (fun q : (L₁.compositum L₂).extensionQuotient ↦
      (compositumRestrictionLeft L₁ L₂ q,
        compositumRestrictionRight L₁ L₂ q)) := by
  intro x y
  revert y
  refine (L₁.compositum L₂).extensionQuotient_inductionOn
    (motive := fun x ↦ ∀ y,
      (compositumRestrictionLeft L₁ L₂ x,
        compositumRestrictionRight L₁ L₂ x) =
          (compositumRestrictionLeft L₁ L₂ y,
            compositumRestrictionRight L₁ L₂ y) → x = y) x ?_
  intro a y
  refine (L₁.compositum L₂).extensionQuotient_inductionOn
    (motive := fun y ↦
      (compositumRestrictionLeft L₁ L₂
          ((L₁.compositum L₂).extensionQuotientMk a),
        compositumRestrictionRight L₁ L₂
          ((L₁.compositum L₂).extensionQuotientMk a)) =
        (compositumRestrictionLeft L₁ L₂ y,
          compositumRestrictionRight L₁ L₂ y) →
        (L₁.compositum L₂).extensionQuotientMk a = y) y ?_
  intro b hab
  have hleft :
      L₁.extensionQuotientMk a = L₁.extensionQuotientMk b :=
    congrArg Prod.fst hab
  have hright :
      L₂.extensionQuotientMk a = L₂.extensionQuotientMk b :=
    congrArg Prod.snd hab
  have hleftRaw := congrArg L₁.extensionQuotientMulEquiv hleft
  have hrightRaw := congrArg L₂.extensionQuotientMulEquiv hright
  simp only [L₁.extensionQuotientMk_apply] at hleftRaw
  simp only [L₂.extensionQuotientMk_apply] at hrightRaw
  apply (L₁.compositum L₂).extensionQuotientMulEquiv.injective
  simp only [FiniteAbelianSubextension.extensionQuotientMk_apply]
  apply QuotientGroup.eq.mpr
  apply (mem_extensionSubgroup_iff K (L₁.compositum L₂).field
    (L₁.compositum L₂).below _).2
  exact ⟨
    (mem_extensionSubgroup_iff K L₁.field L₁.below _).1
      (QuotientGroup.eq.mp hleftRaw),
    (mem_extensionSubgroup_iff K L₂.field L₂.below _).1
      (QuotientGroup.eq.mp hrightRaw)⟩
theorem

ker_compositumRestrictionLeft_inf_ker_compositumRestrictionRight

L356 ↗
ClassFormation.FiniteAbelianSubextension.ker_compositumRestrictionLeft_inf_ker_compositumRestrictionRight
Documentation

Equivalently, the kernels of the two restrictions have trivial intersection. This is the literal group statement used in the first paragraph of the proof of the finite abelian classification theorem.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
theorem ker_compositumRestrictionLeft_inf_ker_compositumRestrictionRight
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L₁ L₂ : FiniteAbelianSubextension K) :
    (compositumRestrictionLeft L₁ L₂).ker ⊓
        (compositumRestrictionRight L₁ L₂).ker = ⊥
theorem

eq_of_le_of_extensionQuotient_card_eq

L382 ↗
ClassFormation.FiniteAbelianSubextension.eq_of_le_of_extensionQuotient_card_eq
Documentation

If one finite abelian extension is contained in another and their actual Galois quotients have the same finite cardinality, then the fields are equal. This is the group-theoretic final step in the injectivity finite classification argument, where equality of cardinalities comes from finite reciprocity.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
theorem eq_of_le_of_extensionQuotient_card_eq
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    {L₁ L₂ : FiniteAbelianSubextension K} (h₁₂ : L₁ ≤ L₂)
    (hcard : Nat.card L₂.extensionQuotient =
      Nat.card L₁.extensionQuotient) :
    L₁ = L₂
theorem

le_iff_normSubgroup_le_of_compositum_and_reciprocity

L419 ↗
ClassFormation.FiniteAbelianSubextension.le_iff_normSubgroup_le_of_compositum_and_reciprocity
Documentation

The order-reversing finite classification argument, kept private until the public the finite abelian classification theorem supplies the compositum formula and the two reciprocity bijectivities from finite reciprocity.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
theorem le_iff_normSubgroup_le_of_compositum_and_reciprocity
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (D : DegreeData G) (A : Rep ℤ G) (v : ValuationData D A)
    (hAxiom : v.SatisfiesUnramifiedUnitCohomology D)
    (K : FiniteAbstractField G)
    (L₁ L₂ : FiniteAbelianSubextension K.field)
    (hcomp : (L₁.compositum L₂).normSubgroup A =
      L₁.normSubgroup A ⊓ L₂.normSubgroup A)
    (hbijP : Function.Bijective
      (D.finiteReciprocityHom A v hAxiom K (L₁.compositum L₂).field
        (L₁.compositum L₂).below))
    (hbij₂ : Function.Bijective
      (D.finiteReciprocityHom A v hAxiom K L₂.field L₂.below)) :
    L₁ ≤ L₂ ↔ L₂.normSubgroup A ≤ L₁.normSubgroup A
theorem

normSubgroup_intersection_eq_sup_of_surjective_and_order

L487 ↗
ClassFormation.FiniteAbelianSubextension.normSubgroup_intersection_eq_sup_of_surjective_and_order
Documentation

The final surjectivity step: surjectivity and order reversal turn the unconditional inclusion for an intersection field into equality.

Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- 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}
local instance extensionQuotient_normal
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    (extensionSubgroup K L.field L.below).Normal :=
  L.normal
local instance representedQuotient_finite
    {G : Type*} [Group G] [TopologicalSpace G] {K : ClosedSubgroup G}
    (L : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
  L.finite
Lean source · statement
theorem normSubgroup_intersection_eq_sup_of_surjective_and_order
    [IsTopologicalGroup G] [CompactSpace G]
    (A : Rep ℤ G) (K : ClosedSubgroup G)
    (L₁ L₂ : FiniteAbelianSubextension K)
    (hsurjective : ∀ H : AddSubgroup (ambientFixedAddSubgroup A K),
      IsNormOpen A K (H : Set (ambientFixedAddSubgroup A K)) →
        ∃ L : FiniteAbelianSubextension K, L.normSubgroup A = H)
    (horder : ∀ X Y : FiniteAbelianSubextension K,
      X ≤ Y ↔ Y.normSubgroup A ≤ X.normSubgroup A) :
    (L₁.intersection L₂).normSubgroup A =
      L₁.normSubgroup A ⊔ L₂.normSubgroup A
instance

classification_extensionQuotient_finite

L522 ↗
ClassFormation.FiniteGaloisSubextension.classification_extensionQuotient_finite
Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

classification_abelianExtension_normal

L527 ↗
ClassFormation.FiniteGaloisSubextension.classification_abelianExtension_normal
Source context 7 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

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

classification_abelianExtension_finite

L532 ↗
ClassFormation.FiniteGaloisSubextension.classification_abelianExtension_finite
Source context 8 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G} [IsTopologicalGroup G]
local instance classification_extensionQuotient_finite
    (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite
local instance classification_abelianExtension_normal
    (M : FiniteAbelianSubextension K) :
    (extensionSubgroup K M.field M.below).Normal :=
  M.normal
Lean source · statement
instance classification_abelianExtension_finite
    (M : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K M.field M.below)
theorem

classFieldCandidate_field_le

L539 ↗
ClassFormation.FiniteGaloisSubextension.classFieldCandidate_field_le
Documentation

The original finite Galois field lies below the abelian class-field candidate cut out inside it.

Source context 9 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G} [IsTopologicalGroup G]
local instance classification_extensionQuotient_finite
    (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite
local instance classification_abelianExtension_normal
    (M : FiniteAbelianSubextension K) :
    (extensionSubgroup K M.field M.below).Normal :=
  M.normal
local instance classification_abelianExtension_finite
    (M : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K M.field M.below) :=
  M.finite
Lean source · statement
theorem classFieldCandidate_field_le
    (E : FiniteGaloisSubextension K) (A : Rep ℤ G)
    (H : AddSubgroup (ambientFixedAddSubgroup A K))
    (rE : FiniteNormQuotient A K E.field E.below ≃+
      Additive (Abelianization E.extensionQuotient)) :
    E.field.toSubgroup ≤
      (ClassFormation.FiniteGaloisSubextension.classFieldCandidate A E H rE).field.toSubgroup
theorem

classFieldCandidate_restriction_eq_one_iff

L552 ↗
ClassFormation.FiniteGaloisSubextension.classFieldCandidate_restriction_eq_one_iff
Documentation

Restriction from E/K to its class-field candidate is trivial exactly on the pulled-back subgroup used to define that candidate.

Source context 9 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G} [IsTopologicalGroup G]
local instance classification_extensionQuotient_finite
    (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite
local instance classification_abelianExtension_normal
    (M : FiniteAbelianSubextension K) :
    (extensionSubgroup K M.field M.below).Normal :=
  M.normal
local instance classification_abelianExtension_finite
    (M : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K M.field M.below) :=
  M.finite
Lean source · statement
theorem classFieldCandidate_restriction_eq_one_iff
    (E : FiniteGaloisSubextension K) (A : Rep ℤ G)
    (H : AddSubgroup (ambientFixedAddSubgroup A K))
    (rE : FiniteNormQuotient A K E.field E.below ≃+
      Additive (Abelianization E.extensionQuotient))
    (q : E.extensionQuotient) :
    abstractReciprocityRestriction K
        (ClassFormation.FiniteGaloisSubextension.classFieldCandidate A E H rE).field E.field
        (classFieldCandidate_field_le E A H rE)
        (ClassFormation.FiniteGaloisSubextension.classFieldCandidate A E H rE).below q = 1 ↔
      q ∈ reciprocityPreimageSubgroup A E H rE
theorem

classFieldCandidate_normSubgroup_eq_of_reciprocity

L599 ↗
ClassFormation.FiniteGaloisSubextension.classFieldCandidate_normSubgroup_eq_of_reciprocity
Documentation

The finite classification surjectivity diagram chase. The final public theorem feeds rE and its compatibility from finite reciprocity, so neither appears as an assumption of the classification endpoint.

Source context 9 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G} [IsTopologicalGroup G]
local instance classification_extensionQuotient_finite
    (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite
local instance classification_abelianExtension_normal
    (M : FiniteAbelianSubextension K) :
    (extensionSubgroup K M.field M.below).Normal :=
  M.normal
local instance classification_abelianExtension_finite
    (M : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K M.field M.below) :=
  M.finite
Lean source · statement
theorem classFieldCandidate_normSubgroup_eq_of_reciprocity
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (D : DegreeData G) (A : Rep ℤ G) (v : ValuationData D A)
    (hAxiom : v.SatisfiesUnramifiedUnitCohomology D)
    (K : FiniteAbstractField G)
    (E : FiniteGaloisSubextension K.field)
    (H : AddSubgroup (ambientFixedAddSubgroup A K.field))
    (hEH : ClassFormation.FiniteGaloisSubextension.normSubgroup A E ≤ H)
    (rE : FiniteNormQuotient A K.field E.field E.below ≃+
      Additive (Abelianization E.extensionQuotient))
    (hcompatE : ∀ q : E.extensionQuotient,
      rE.symm (Additive.ofMul (Abelianization.of q)) =
        D.finiteReciprocityHom A v hAxiom K E.field E.below
          (Additive.ofMul q))
    (hbijM : Function.Bijective
      (D.finiteReciprocityHom A v hAxiom K
        (ClassFormation.FiniteGaloisSubextension.classFieldCandidate A E H rE).field
        (ClassFormation.FiniteGaloisSubextension.classFieldCandidate A E H rE).below)) :
    (ClassFormation.FiniteGaloisSubextension.classFieldCandidate A E H rE).normSubgroup A = H
theorem

upperQuotientEquiv_quotientMk_eq_restriction

L715 ↗
ClassFormation.FiniteGaloisSubextension.upperQuotientEquiv_quotientMk_eq_restriction
Documentation

The third-isomorphism quotient by S is literally restriction from E / K to the intermediate field fixed by S. This representative-level identity connects the candidate quotient in the surjectivity construction of the finite abelian classification theorem to restriction compatibility's restriction map.

Source context 9 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G} [IsTopologicalGroup G]
local instance classification_extensionQuotient_finite
    (E : FiniteGaloisSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K E.field E.below) :=
  E.finite
local instance classification_abelianExtension_normal
    (M : FiniteAbelianSubextension K) :
    (extensionSubgroup K M.field M.below).Normal :=
  M.normal
local instance classification_abelianExtension_finite
    (M : FiniteAbelianSubextension K) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K M.field M.below) :=
  M.finite
Lean source · full declaration
theorem upperQuotientEquiv_quotientMk_eq_restriction
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {K : ClosedSubgroup G}
    (E : FiniteGaloisSubextension K) (S : Subgroup E.extensionQuotient)
    [hS : S.Normal] (q : E.extensionQuotient) :
    letI : (extensionSubgroup K E.field E.below).Normal := E.normal
    letI : (extensionSubgroup K (E.intermediateField S)
      (E.intermediateField_le_base S)).Normal :=
      E.intermediateField_normal S hS
    E.upperQuotientEquiv S (QuotientGroup.mk q) =
      abstractReciprocityRestriction K (E.intermediateField S) E.field
        (E.field_le_intermediateField S)
        (E.intermediateField_le_base S) q := by
  let : (extensionSubgroup K E.field E.below).Normal := E.normal
  let : (extensionSubgroup K (E.intermediateField S)
      (E.intermediateField_le_base S)).Normal :=
    E.intermediateField_normal S hS
  refine QuotientGroup.induction_on q ?_
  intro k
  exact E.upperQuotientEquiv_mk_mk S k
theorem

reciprocityEquiv_bijective

L754 ↗
ClassFormation.FiniteAbelianSubextension.reciprocityEquiv_bijective
Documentation

finite reciprocity specialized to an actual finite abelian extension. The two halves are supplied by the general Sylow surjectivity argument and the cyclic-coordinate injectivity argument; no bijectivity premise is exposed by the finite abelian classification theorem.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · full declaration
theorem reciprocityEquiv_bijective
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (hAxiom : v.SatisfiesUnramifiedUnitCohomology D)
    (K : FiniteAbstractField G)
    (L : FiniteAbelianSubextension K.field) :
    letI : Finite
        (K.field.toSubgroup ⧸
          extensionSubgroup K.field L.field L.below) := L.finite
    Function.Bijective
      (D.finiteReciprocityHom A v hAxiom K L.field L.below) := by
  let : (extensionSubgroup K.field L.field L.below).Normal := L.normal
  let : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L.field L.below) := L.finite
  let : IsMulCommutative L.toFiniteGaloisExtension.extensionQuotient :=
    L.commutative
  exact ⟨
    v.abstractReciprocity_abelian_finiteReciprocityHom_injective
      hcf hAxiom K L.toFiniteGaloisExtension,
    v.abstractReciprocity_finiteReciprocityHom_surjective
      hcf hAxiom K L.toFiniteGaloisExtension⟩
theorem

normSubgroup_compositum

L782 ↗
ClassFormation.FiniteAbelianSubextension.normSubgroup_compositum
Documentation

The first displayed formula in the finite abelian classification theorem: the norm subgroup of the compositum is the intersection of the two norm subgroups. This is the first paragraph of the finite classification proof, with finite reciprocity supplying all three vertical isomorphisms.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem normSubgroup_compositum
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (L₁ L₂ : FiniteAbelianSubextension K.field) :
    (L₁.compositum L₂).normSubgroup A =
      L₁.normSubgroup A ⊓ L₂.normSubgroup A
theorem

le_iff_normSubgroup_le

L803 ↗
ClassFormation.FiniteAbelianSubextension.le_iff_normSubgroup_le
Documentation

The order-reversal assertion in the finite abelian classification theorem: field inclusion is exactly reverse inclusion of norm subgroups.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem le_iff_normSubgroup_le
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (L₁ L₂ : FiniteAbelianSubextension K.field) :
    L₁ ≤ L₂ ↔ L₂.normSubgroup A ≤ L₁.normSubgroup A
theorem

normSubgroupMap_injective

L820 ↗
ClassFormation.FiniteAbelianSubextension.normSubgroupMap_injective
Documentation

The forward map in the finite abelian classification theorem is injective.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem normSubgroupMap_injective
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G) :
    Function.Injective (normSubgroupMap A :
      FiniteAbelianSubextension K.field → NormOpenAddSubgroup A K.field)
theorem

classFieldCandidate_normSubgroup_eq

L840 ↗
ClassFormation.FiniteAbelianSubextension.classFieldCandidate_normSubgroup_eq
Documentation

The kernel equality in the surjectivity surjectivity step. Starting from N_E ≤ H, pull H / N_E back through the actual norm-residue symbol of finite reciprocity and take its fixed field. The norm subgroup of that concrete finite abelian candidate is exactly H.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · full declaration
theorem classFieldCandidate_normSubgroup_eq
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (E : FiniteGaloisSubextension K.field)
    (H : AddSubgroup (ambientFixedAddSubgroup A K.field))
    (hEH : ClassFormation.FiniteGaloisSubextension.normSubgroup A E ≤ H) :
    let rE := D.normResidueSymbol A v hcf K E
    (ClassFormation.FiniteGaloisSubextension.classFieldCandidate A E H rE).normSubgroup A = H := by
  dsimp only
  let : (extensionSubgroup K.field E.field E.below).Normal := E.normal
  let : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field E.field E.below) := E.finite
  let hAxiom := v.classFieldAxiom_implies_unramifiedUnitCohomology hcf
  let rE := D.normResidueSymbol A v hcf K E
  let M := ClassFormation.FiniteGaloisSubextension.classFieldCandidate A E H rE
  have hcompatE (q : E.extensionQuotient) :
      rE.symm (Additive.ofMul (Abelianization.of q)) =
        D.finiteReciprocityHom A v hAxiom K E.field E.below
          (Additive.ofMul q) := by
    simpa only [rE, DegreeData.normResidueSymbol, AddEquiv.symm_symm] using
      D.abstractReciprocityEquiv_apply_of A v hcf K E q
  exact
    FiniteGaloisSubextension.classFieldCandidate_normSubgroup_eq_of_reciprocity
      D A v hAxiom K E H hEH rE hcompatE
        (reciprocityEquiv_bijective
          v hcf hAxiom K M)
theorem

normSubgroupMap_surjective

L873 ↗
ClassFormation.FiniteAbelianSubextension.normSubgroupMap_surjective
Documentation

Every open subgroup in the norm topology is the norm subgroup of an actual finite abelian extension. The extension is the fixed field of the literal preimage of H / N_E under the norm-residue symbol of finite reciprocity.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem normSubgroupMap_surjective
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G) :
    Function.Surjective (normSubgroupMap A :
      FiniteAbelianSubextension K.field → NormOpenAddSubgroup A K.field)
theorem

normSubgroupMap_bijective

L897 ↗
ClassFormation.FiniteAbelianSubextension.normSubgroupMap_bijective
Documentation

The norm-subgroup map of the finite abelian classification theorem is bijective.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem normSubgroupMap_bijective
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G) :
    Function.Bijective (normSubgroupMap A :
      FiniteAbelianSubextension K.field → NormOpenAddSubgroup A K.field)
def

normSubgroupOrderIso

L910 ↗
ClassFormation.FiniteAbelianSubextension.normSubgroupOrderIso
Documentation

the finite abelian classification theorem. Finite abelian extensions of the base are order-isomorphic to the opposite poset of norm-open subgroups.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · full declaration
def normSubgroupOrderIso
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G) :
    FiniteAbelianSubextension K.field ≃o (NormOpenAddSubgroup A K.field)ᵒᵈ where
  toEquiv := Equiv.ofBijective (normSubgroupMap A)
    (normSubgroupMap_bijective v hcf K)
  map_rel_iff' := by
    intro L₁ L₂
    change L₂.normSubgroup A ≤ L₁.normSubgroup A ↔ L₁ ≤ L₂
    exact (le_iff_normSubgroup_le v hcf K L₁ L₂).symm
theorem

normSubgroupOrderIso_apply

L928 ↗
ClassFormation.FiniteAbelianSubextension.normSubgroupOrderIso_apply
Documentation

The defining evaluation formula for normSubgroupOrderIso is (OrderDual.ofDual (normSubgroupOrderIso v hcf K L)).1 = L.normSubgroup A.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem normSubgroupOrderIso_apply
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (L : FiniteAbelianSubextension K.field) :
    (OrderDual.ofDual (normSubgroupOrderIso v hcf K L)).1 =
      L.normSubgroup A
theorem

normSubgroup_intersection

L942 ↗
ClassFormation.FiniteAbelianSubextension.normSubgroup_intersection
Documentation

The second displayed formula in the finite abelian classification theorem: the norm subgroup of the intersection field is the product of the two norm subgroups (their supremum in additive notation).

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteAbelianSubextension
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem normSubgroup_intersection
    (v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : FiniteAbstractField G)
    (L₁ L₂ : FiniteAbelianSubextension K.field) :
    (L₁.intersection L₂).normSubgroup A =
      L₁.normSubgroup A ⊔ L₂.normSubgroup A

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.