NYLL
Module

InfiniteAbelianClassFieldCorrespondence.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.InfiniteAbelianClassFieldCorrespondence
9 declarations indexed from sourceView source ↗

Module documentation

Infinite abelian class-field correspondence

Maximal abelian reciprocity transports closed subgroups of the idele-class component quotient to closed subgroups of the maximal abelian Galois group. Composing this transport with the infinite Galois correspondence gives the order-reversing infinite abelian class-field correspondence.

Imports1
Imported by2

Declarations

def

mapContinuousMulEquiv

L32 ↗
ClosedSubgroup.mapContinuousMulEquiv
Documentation

Transport a closed subgroup along a continuous multiplicative equivalence.

Source context 4 commands

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

open scoped NumberField
noncomputable section
namespace ClosedSubgroup
variable {G H : Type*}
  [Group G] [TopologicalSpace G]
  [Group H] [TopologicalSpace H]
Lean source · full declaration
def mapContinuousMulEquiv
    (e : G ≃ₜ* H) (S : ClosedSubgroup G) : ClosedSubgroup H where
  toSubgroup := e.toMulEquiv.mapSubgroup S.toSubgroup
  isClosed' := by
    change IsClosed (e '' (S : Set G))
    exact e.toHomeomorph.isClosedMap (S : Set G) S.isClosed'
def

orderIsoMapContinuousMulEquiv

L41 ↗
ClosedSubgroup.orderIsoMapContinuousMulEquiv
Documentation

A continuous multiplicative equivalence induces an order equivalence on closed subgroups.

Source context 4 commands

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

open scoped NumberField
noncomputable section
namespace ClosedSubgroup
variable {G H : Type*}
  [Group G] [TopologicalSpace G]
  [Group H] [TopologicalSpace H]
Lean source · full declaration
def orderIsoMapContinuousMulEquiv
    (e : G ≃ₜ* H) : ClosedSubgroup G ≃o ClosedSubgroup H where
  toFun := mapContinuousMulEquiv e
  invFun := mapContinuousMulEquiv e.symm
  left_inv S := by
    apply ClosedSubgroup.toSubgroup_injective
    change
      e.symm.toMulEquiv.mapSubgroup
          (e.toMulEquiv.mapSubgroup S.toSubgroup) =
        S.toSubgroup
    exact e.toMulEquiv.mapSubgroup.left_inv S.toSubgroup
  right_inv T := by
    apply ClosedSubgroup.toSubgroup_injective
    change
      e.toMulEquiv.mapSubgroup
          (e.symm.toMulEquiv.mapSubgroup T.toSubgroup) =
        T.toSubgroup
    exact e.toMulEquiv.mapSubgroup.right_inv T.toSubgroup
  map_rel_iff' {S T} := by
    change
      e.toMulEquiv.mapSubgroup S.toSubgroup ≤
          e.toMulEquiv.mapSubgroup T.toSubgroup ↔
        S.toSubgroup ≤ T.toSubgroup
    exact e.toMulEquiv.mapSubgroup.le_iff_le
def

orderDualIsoMapContinuousMulEquiv

L67 ↗
ClosedSubgroup.orderDualIsoMapContinuousMulEquiv
Documentation

The order-dual form of closed-subgroup transport.

Source context 4 commands

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

open scoped NumberField
noncomputable section
namespace ClosedSubgroup
variable {G H : Type*}
  [Group G] [TopologicalSpace G]
  [Group H] [TopologicalSpace H]
Lean source · full declaration
def orderDualIsoMapContinuousMulEquiv
    (e : G ≃ₜ* H) :
    (ClosedSubgroup G)ᵒᵈ ≃o (ClosedSubgroup H)ᵒᵈ where
  toFun S := OrderDual.toDual
    (mapContinuousMulEquiv e (OrderDual.ofDual S))
  invFun T := OrderDual.toDual
    (mapContinuousMulEquiv e.symm (OrderDual.ofDual T))
  left_inv S := by
    exact congrArg OrderDual.toDual
      ((orderIsoMapContinuousMulEquiv e).left_inv (OrderDual.ofDual S))
  right_inv T := by
    exact congrArg OrderDual.toDual
      ((orderIsoMapContinuousMulEquiv e).right_inv (OrderDual.ofDual T))
  map_rel_iff' {S T} := by
    change
      mapContinuousMulEquiv e (OrderDual.ofDual T) ≤
          mapContinuousMulEquiv e (OrderDual.ofDual S) ↔
        OrderDual.ofDual T ≤ OrderDual.ofDual S
    exact (orderIsoMapContinuousMulEquiv e).le_iff_le
theorem

coe_mapContinuousMulEquiv

L88 ↗
ClosedSubgroup.coe_mapContinuousMulEquiv
Source context 4 commands

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

open scoped NumberField
noncomputable section
namespace ClosedSubgroup
variable {G H : Type*}
  [Group G] [TopologicalSpace G]
  [Group H] [TopologicalSpace H]
Lean source · statement
theorem coe_mapContinuousMulEquiv
    (e : G ≃ₜ* H) (S : ClosedSubgroup G) :
    (mapContinuousMulEquiv e S : Set H) = e '' (S : Set G)
def

infiniteAbelianClassFieldCorrespondence

L108 ↗
GlobalClassFieldTheory.GlobalClassFields.infiniteAbelianClassFieldCorrespondence
Documentation

The infinite abelian class-field correspondence. The order dual in the domain records that larger closed idele-class subgroups correspond to smaller intermediate fields.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def infiniteAbelianClassFieldCorrespondence :
    (ClosedSubgroup (ideleClassComponentQuotient K))ᵒᵈ ≃o
      IntermediateField K (maximalAbelianExtension K)
theorem

infiniteAbelianClassFieldCorrespondence_apply

L119 ↗
GlobalClassFieldTheory.GlobalClassFields.infiniteAbelianClassFieldCorrespondence_apply
Documentation

Forward evaluation is the fixed field of the transported closed idele-class subgroup.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem infiniteAbelianClassFieldCorrespondence_apply
    (H : ClosedSubgroup (ideleClassComponentQuotient K)) :
    infiniteAbelianClassFieldCorrespondence K (OrderDual.toDual H) =
      IntermediateField.fixedField
        (ClosedSubgroup.mapContinuousMulEquiv
          (ideleClassComponentQuotientEquivMaximalAbelianGalois K) H)
theorem

infiniteAbelianClassFieldCorrespondence_symm_apply

L130 ↗
GlobalClassFieldTheory.GlobalClassFields.infiniteAbelianClassFieldCorrespondence_symm_apply
Documentation

The inverse correspondence is the fixing subgroup transported back to the idele-class component quotient.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem infiniteAbelianClassFieldCorrespondence_symm_apply
    (L : IntermediateField K (maximalAbelianExtension K)) :
    (infiniteAbelianClassFieldCorrespondence K).symm L =
      OrderDual.toDual
        (ClosedSubgroup.mapContinuousMulEquiv
          (ideleClassComponentQuotientEquivMaximalAbelianGalois K).symm
          { toSubgroup := L.fixingSubgroup
            isClosed' := InfiniteGalois.fixingSubgroup_isClosed L })
theorem

infiniteAbelianClassFieldCorrespondence_fixingSubgroup

L142 ↗
GlobalClassFieldTheory.GlobalClassFields.infiniteAbelianClassFieldCorrespondence_fixingSubgroup
Documentation

The fixing subgroup of the field corresponding to H is exactly the transport of H by maximal abelian reciprocity.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem infiniteAbelianClassFieldCorrespondence_fixingSubgroup
    (H : ClosedSubgroup (ideleClassComponentQuotient K)) :
    (infiniteAbelianClassFieldCorrespondence K
        (OrderDual.toDual H)).fixingSubgroup =
      (ClosedSubgroup.mapContinuousMulEquiv
        (ideleClassComponentQuotientEquivMaximalAbelianGalois K) H).toSubgroup
theorem

infiniteAbelianClassFieldCorrespondence_finite_iff_open

L153 ↗
GlobalClassFieldTheory.GlobalClassFields.infiniteAbelianClassFieldCorrespondence_finite_iff_open
Documentation

A field in the infinite abelian correspondence is finite over the base exactly when the corresponding closed idele-class subgroup is open.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem infiniteAbelianClassFieldCorrespondence_finite_iff_open
    (H : ClosedSubgroup (ideleClassComponentQuotient K)) :
    FiniteDimensional K
        (infiniteAbelianClassFieldCorrespondence K
          (OrderDual.toDual H)) ↔
      IsOpen (H : Set (ideleClassComponentQuotient K))

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