NYLL
Module

FiniteReciprocityDiagram.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.FiniteReciprocityDiagram
14 declarations indexed from sourceView source ↗

Module documentation

Finite reciprocity as an isomorphism of diagrams

The open normal subgroups of the absolute abelianized Galois group index three covariant finite diagrams: its finite quotients, the corresponding finite abelian Galois groups, and the corresponding norm quotients. This file packages the canonical finite-stage identifications as natural isomorphisms.

Imports2
Imported by1

Declarations

abbrev

AbsoluteFiniteIndex

L30 ↗
LocalClassFieldTheory.AbsoluteFiniteIndex
Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
abbrev AbsoluteFiniteIndex
instance

finiteDiagramNormQuotientTopologicalSpace

L33 ↗
LocalClassFieldTheory.finiteDiagramNormQuotientTopologicalSpace
Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
instance finiteDiagramNormQuotientTopologicalSpace
    (E L : Type) [Field E] [Field L] [Algebra E L]
    [TopologicalSpace E] :
    TopologicalSpace (NormQuotient E L)
instance

finiteDiagramNormQuotientIsTopologicalGroup

L40 ↗
LocalClassFieldTheory.finiteDiagramNormQuotientIsTopologicalGroup
Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
noncomputable local instance finiteDiagramNormQuotientTopologicalSpace
    (E L : Type) [Field E] [Field L] [Algebra E L]
    [TopologicalSpace E] :
    TopologicalSpace (NormQuotient E L) := by
  change TopologicalSpace (Eˣ ⧸ localNormSubgroup E L)
  infer_instance
Lean source · statement
instance finiteDiagramNormQuotientIsTopologicalGroup
    (L : Type) [Field L] [Algebra K L] :
    IsTopologicalGroup (NormQuotient K L)
def

absoluteFiniteQuotientDiagram

L48 ↗
LocalClassFieldTheory.absoluteFiniteQuotientDiagram
Documentation

The finite quotients of the absolute abelianized Galois group, carrying their quotient topologies and the canonical quotient transition maps.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
noncomputable local instance finiteDiagramNormQuotientTopologicalSpace
    (E L : Type) [Field E] [Field L] [Algebra E L]
    [TopologicalSpace E] :
    TopologicalSpace (NormQuotient E L) := by
  change TopologicalSpace (Eˣ ⧸ localNormSubgroup E L)
  infer_instance
local instance finiteDiagramNormQuotientIsTopologicalGroup
    (L : Type) [Field L] [Algebra K L] :
    IsTopologicalGroup (NormQuotient K L) := by
  change IsTopologicalGroup (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
Lean source · full declaration
def absoluteFiniteQuotientDiagram :
    AbsoluteFiniteIndex K ⥤ ProfiniteGrp where
  obj N := ProfiniteGrp.of
    (localAbsoluteAbelianProfinite K ⧸ N.toSubgroup)
  map f := ProfiniteGrp.ofHom <|
    absoluteFiniteQuotientTransition (leOfHom f)
  map_id N := by
    apply ProfiniteGrp.hom_ext
    apply ContinuousMonoidHom.ext
    intro x
    refine QuotientGroup.induction_on x ?_
    intro x
    rfl
  map_comp {X Y Z} f g := by
    apply ProfiniteGrp.hom_ext
    apply ContinuousMonoidHom.ext
    intro x
    refine QuotientGroup.induction_on x ?_
    intro x
    rfl
def

finiteAbelianGaloisDiagram

L70 ↗
LocalClassFieldTheory.finiteAbelianGaloisDiagram
Documentation

The finite abelian Galois groups cut out by open normal subgroups of the absolute abelianized Galois group, with restriction as transition map.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
noncomputable local instance finiteDiagramNormQuotientTopologicalSpace
    (E L : Type) [Field E] [Field L] [Algebra E L]
    [TopologicalSpace E] :
    TopologicalSpace (NormQuotient E L) := by
  change TopologicalSpace (Eˣ ⧸ localNormSubgroup E L)
  infer_instance
local instance finiteDiagramNormQuotientIsTopologicalGroup
    (L : Type) [Field L] [Algebra K L] :
    IsTopologicalGroup (NormQuotient K L) := by
  change IsTopologicalGroup (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
Lean source · full declaration
def finiteAbelianGaloisDiagram :
    AbsoluteFiniteIndex K ⥤ ProfiniteGrp where
  obj N := ProfiniteGrp.of
    (Gal(absoluteFiniteQuotientField K N / K))
  map {N M} f := ProfiniteGrp.ofHom <|
    intermediateFieldRestrictContinuous K
      (absoluteFiniteQuotientField K M)
      (absoluteFiniteQuotientField K N)
      (absoluteFiniteQuotientField_antitone (leOfHom f))
  map_id N := by
    apply ProfiniteGrp.hom_ext
    apply ContinuousMonoidHom.ext
    intro sigma
    apply AlgEquiv.ext
    intro x
    apply Subtype.ext
    exact intermediateFieldRestrictNormalHom_apply_val
      (absoluteFiniteQuotientField K N)
      (absoluteFiniteQuotientField K N) le_rfl sigma x
  map_comp {N M L} f g := by
    apply ProfiniteGrp.hom_ext
    apply ContinuousMonoidHom.ext
    intro sigma
    apply AlgEquiv.ext
    intro x
    apply Subtype.ext
    change
      (absoluteFiniteQuotientField K L).val
        (intermediateFieldRestrictNormalHom
          (absoluteFiniteQuotientField K L)
          (absoluteFiniteQuotientField K N) _ sigma x) =
      (absoluteFiniteQuotientField K L).val
        (intermediateFieldRestrictNormalHom
          (absoluteFiniteQuotientField K L)
          (absoluteFiniteQuotientField K M) _
          (intermediateFieldRestrictNormalHom
            (absoluteFiniteQuotientField K M)
            (absoluteFiniteQuotientField K N) _ sigma) x)
    rw [intermediateFieldRestrictNormalHom_apply_val]
    rw [intermediateFieldRestrictNormalHom_apply_val]
    rw [intermediateFieldRestrictNormalHom_apply_val]
    apply congrArg (fun y : absoluteFiniteQuotientField K N =>
      (absoluteFiniteQuotientField K N).val (sigma y))
    apply Subtype.ext
    rfl
def

absoluteFiniteQuotientNaturalIso

L119 ↗
LocalClassFieldTheory.absoluteFiniteQuotientNaturalIso
Documentation

At every finite stage, the quotient of the absolute abelianized Galois group is canonically the Galois group of its fixed field; these identifications commute with all transition maps.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
noncomputable local instance finiteDiagramNormQuotientTopologicalSpace
    (E L : Type) [Field E] [Field L] [Algebra E L]
    [TopologicalSpace E] :
    TopologicalSpace (NormQuotient E L) := by
  change TopologicalSpace (Eˣ ⧸ localNormSubgroup E L)
  infer_instance
local instance finiteDiagramNormQuotientIsTopologicalGroup
    (L : Type) [Field L] [Algebra K L] :
    IsTopologicalGroup (NormQuotient K L) := by
  change IsTopologicalGroup (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
Lean source · statement
def absoluteFiniteQuotientNaturalIso :
    absoluteFiniteQuotientDiagram K ≅ finiteAbelianGaloisDiagram K
theorem

absoluteFiniteNormSubgroup_mono

L135 ↗
LocalClassFieldTheory.absoluteFiniteNormSubgroup_mono
Documentation

Inclusion of open normal subgroups gives the corresponding inclusion of finite norm subgroups.

Source context 8 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
noncomputable local instance finiteDiagramNormQuotientTopologicalSpace
    (E L : Type) [Field E] [Field L] [Algebra E L]
    [TopologicalSpace E] :
    TopologicalSpace (NormQuotient E L) := by
  change TopologicalSpace (Eˣ ⧸ localNormSubgroup E L)
  infer_instance
local instance finiteDiagramNormQuotientIsTopologicalGroup
    (L : Type) [Field L] [Algebra K L] :
    IsTopologicalGroup (NormQuotient K L) := by
  change IsTopologicalGroup (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem absoluteFiniteNormSubgroup_mono
    {N M : AbsoluteFiniteIndex K} (hNM : N ≤ M) :
    localNormSubgroup K (absoluteFiniteQuotientField K N) ≤
      localNormSubgroup K (absoluteFiniteQuotientField K M)
def

absoluteFiniteArtinQuotientEquiv

L156 ↗
LocalClassFieldTheory.absoluteFiniteArtinQuotientEquiv
Documentation

The first isomorphism theorem for a finite coordinate of the absolute Artin map, with its kernel identified with the corresponding norm subgroup.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
noncomputable local instance finiteDiagramNormQuotientTopologicalSpace
    (E L : Type) [Field E] [Field L] [Algebra E L]
    [TopologicalSpace E] :
    TopologicalSpace (NormQuotient E L) := by
  change TopologicalSpace (Eˣ ⧸ localNormSubgroup E L)
  infer_instance
local instance finiteDiagramNormQuotientIsTopologicalGroup
    (L : Type) [Field L] [Algebra K L] :
    IsTopologicalGroup (NormQuotient K L) := by
  change IsTopologicalGroup (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
Lean source · statement
def absoluteFiniteArtinQuotientEquiv
    (N : AbsoluteFiniteIndex K) :
    NormQuotient K (absoluteFiniteQuotientField K N) ≃ₜ*
      (localAbsoluteAbelianProfinite K ⧸ N.toSubgroup)
theorem

absoluteFiniteArtinQuotientEquiv_mk

L179 ↗
LocalClassFieldTheory.absoluteFiniteArtinQuotientEquiv_mk
Documentation

States the theorem absoluteFiniteArtinQuotientEquiv_mk.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
noncomputable local instance finiteDiagramNormQuotientTopologicalSpace
    (E L : Type) [Field E] [Field L] [Algebra E L]
    [TopologicalSpace E] :
    TopologicalSpace (NormQuotient E L) := by
  change TopologicalSpace (Eˣ ⧸ localNormSubgroup E L)
  infer_instance
local instance finiteDiagramNormQuotientIsTopologicalGroup
    (L : Type) [Field L] [Algebra K L] :
    IsTopologicalGroup (NormQuotient K L) := by
  change IsTopologicalGroup (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
Lean source · statement
theorem absoluteFiniteArtinQuotientEquiv_mk
    (N : AbsoluteFiniteIndex K) (a : Kˣ) :
    absoluteFiniteArtinQuotientEquiv K N
        (normClass K
          (absoluteFiniteQuotientField K N) a) =
      absoluteFiniteArtinMap K N a
def

normQuotientTransition

L191 ↗
LocalClassFieldTheory.normQuotientTransition
Documentation

The transition map on norm quotients induced by a tower of fixed fields.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
noncomputable local instance finiteDiagramNormQuotientTopologicalSpace
    (E L : Type) [Field E] [Field L] [Algebra E L]
    [TopologicalSpace E] :
    TopologicalSpace (NormQuotient E L) := by
  change TopologicalSpace (Eˣ ⧸ localNormSubgroup E L)
  infer_instance
local instance finiteDiagramNormQuotientIsTopologicalGroup
    (L : Type) [Field L] [Algebra K L] :
    IsTopologicalGroup (NormQuotient K L) := by
  change IsTopologicalGroup (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
Lean source · statement
def normQuotientTransition
    {N M : AbsoluteFiniteIndex K} (hNM : N ≤ M) :
    NormQuotient K (absoluteFiniteQuotientField K N) →ₜ*
      NormQuotient K (absoluteFiniteQuotientField K M)
theorem

normQuotientTransition_mk

L210 ↗
LocalClassFieldTheory.normQuotientTransition_mk
Documentation

States the theorem normQuotientTransition_mk.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
noncomputable local instance finiteDiagramNormQuotientTopologicalSpace
    (E L : Type) [Field E] [Field L] [Algebra E L]
    [TopologicalSpace E] :
    TopologicalSpace (NormQuotient E L) := by
  change TopologicalSpace (Eˣ ⧸ localNormSubgroup E L)
  infer_instance
local instance finiteDiagramNormQuotientIsTopologicalGroup
    (L : Type) [Field L] [Algebra K L] :
    IsTopologicalGroup (NormQuotient K L) := by
  change IsTopologicalGroup (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
Lean source · statement
theorem normQuotientTransition_mk
    {N M : AbsoluteFiniteIndex K} (hNM : N ≤ M) (a : Kˣ) :
    normQuotientTransition K hNM
        (normClass K
          (absoluteFiniteQuotientField K N) a) =
      normClass K
        (absoluteFiniteQuotientField K M) a
def

normQuotientDiagram

L224 ↗
LocalClassFieldTheory.normQuotientDiagram
Documentation

The finite norm quotients indexed by open normal subgroups, with the canonical quotient maps induced by inclusions of norm subgroups.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
noncomputable local instance finiteDiagramNormQuotientTopologicalSpace
    (E L : Type) [Field E] [Field L] [Algebra E L]
    [TopologicalSpace E] :
    TopologicalSpace (NormQuotient E L) := by
  change TopologicalSpace (Eˣ ⧸ localNormSubgroup E L)
  infer_instance
local instance finiteDiagramNormQuotientIsTopologicalGroup
    (L : Type) [Field L] [Algebra K L] :
    IsTopologicalGroup (NormQuotient K L) := by
  change IsTopologicalGroup (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
Lean source · full declaration
def normQuotientDiagram :
    AbsoluteFiniteIndex K ⥤ ProfiniteGrp where
  obj N := ProfiniteGrp.ofContinuousMulEquiv
    (G := (absoluteFiniteQuotientDiagram K).obj N)
    (absoluteFiniteArtinQuotientEquiv K N).symm
  map f := ConcreteCategory.ofHom (C := ProfiniteGrp)
    (normQuotientTransition K (leOfHom f))
  map_id N := by
    apply ProfiniteGrp.hom_ext
    apply ContinuousMonoidHom.ext
    intro x
    change normQuotientTransition K (leOfHom (𝟙 N)) x = x
    refine NormQuotient.inductionOn
      (K := K) (L := absoluteFiniteQuotientField K N)
      (motive := fun q =>
        normQuotientTransition K (leOfHom (𝟙 N)) q = q) x ?_
    intro a
    exact normQuotientTransition_mk K (leOfHom (𝟙 N)) a
  map_comp f g := by
    apply ProfiniteGrp.hom_ext
    apply ContinuousMonoidHom.ext
    intro x
    refine NormQuotient.inductionOn
      (K := K)
      (motive := fun q =>
        normQuotientTransition K (leOfHom (f ≫ g)) q =
          normQuotientTransition K (leOfHom g)
            (normQuotientTransition K (leOfHom f) q)) x ?_
    intro a
    rw [normQuotientTransition_mk, normQuotientTransition_mk,
      normQuotientTransition_mk]
def

finiteArtinQuotientNaturalIso

L258 ↗
LocalClassFieldTheory.finiteArtinQuotientNaturalIso
Documentation

The finite Artin first-isomorphism identifications form a natural isomorphism from norm quotients to finite absolute Galois quotients.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
noncomputable local instance finiteDiagramNormQuotientTopologicalSpace
    (E L : Type) [Field E] [Field L] [Algebra E L]
    [TopologicalSpace E] :
    TopologicalSpace (NormQuotient E L) := by
  change TopologicalSpace (Eˣ ⧸ localNormSubgroup E L)
  infer_instance
local instance finiteDiagramNormQuotientIsTopologicalGroup
    (L : Type) [Field L] [Algebra K L] :
    IsTopologicalGroup (NormQuotient K L) := by
  change IsTopologicalGroup (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
Lean source · statement
def finiteArtinQuotientNaturalIso :
    normQuotientDiagram K ≅ absoluteFiniteQuotientDiagram K
def

finiteReciprocityNaturalIso

L298 ↗
LocalClassFieldTheory.finiteReciprocityNaturalIso
Documentation

Finite local reciprocity, simultaneously at every open finite quotient: norm quotients are naturally isomorphic to the corresponding finite abelian Galois groups.

Source context 7 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
noncomputable local instance finiteDiagramNormQuotientTopologicalSpace
    (E L : Type) [Field E] [Field L] [Algebra E L]
    [TopologicalSpace E] :
    TopologicalSpace (NormQuotient E L) := by
  change TopologicalSpace (Eˣ ⧸ localNormSubgroup E L)
  infer_instance
local instance finiteDiagramNormQuotientIsTopologicalGroup
    (L : Type) [Field L] [Algebra K L] :
    IsTopologicalGroup (NormQuotient K L) := by
  change IsTopologicalGroup (Kˣ ⧸ localNormSubgroup K L)
  infer_instance
Lean source · statement
def finiteReciprocityNaturalIso :
    normQuotientDiagram K ≅ finiteAbelianGaloisDiagram K

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