NYLL
Module

CohomologyBridge.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.ClassFormation.CohomologyBridge
28 declarations indexed from sourceView source ↗

Module documentation

The actual low-degree Tate quotients as Herbrand quotients

This file compares the concrete multiplicative Herbrand quotients from low-degree cyclic cohomology with the Tate objects built from mathlib's actual Galois representation on Lˣ. The comparison uses the standard Galois action on units; it does not introduce a replacement coefficient object.

Imports5
Imported by4

Declarations

theorem

unitsNormLinearMap_toMul_eq_tateNorm

L37 ↗
LocalClassFieldTheory.unitsNormLinearMap_toMul_eq_tateNorm
Documentation

The norm in the actual unit representation is the multiplicative Herbrand norm after passing from Additive Lˣ back to Lˣ.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem unitsNormLinearMap_toMul_eq_tateNorm
    [Fintype (Gal(L/K))] (x : Lˣ) :
    Additive.toMul (unitsNormLinearMap K L (Additive.ofMul x)) =
      tateNorm (Gal(L / K)) Lˣ x
def

additiveFixedUnitsEquivInvariants

L62 ↗
LocalClassFieldTheory.additiveFixedUnitsEquivInvariants
Documentation

Multiplicative fixed units and the invariant submodule of the actual unit representation are the same additive group.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · full declaration
def additiveFixedUnitsEquivInvariants :
    Additive (fixedSubgroup (Gal(L / K)) Lˣ) ≃+
      unitsInvariantSubmodule K L where
  toFun x := ⟨Additive.ofMul ((Additive.toMul x : fixedSubgroup (Gal(L / K)) Lˣ) : Lˣ), by
    intro σ
    exact congrArg Additive.ofMul ((Additive.toMul x).property σ)⟩
  invFun x := Additive.ofMul ⟨Additive.toMul (x : Additive Lˣ), by
    intro σ
    exact Additive.ofMul.injective (x.property σ)⟩
  left_inv x := rfl
  right_inv x := rfl
  map_add' x y := rfl
def

additiveEquivToQuotientHom

L80 ↗
LocalClassFieldTheory.additiveEquivToQuotientHom
Documentation

Compose an additive equivalence with a submodule quotient map.

Keeping this construction polymorphic prevents typeclass search from unfolding the concrete Galois representation while it looks for the quotient's additive structure.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def additiveEquivToQuotientHom
    {A M : Type} [AddCommGroup A] [AddCommGroup M]
    (e : A ≃+ M) (N : Submodule ℤ M) : A →+ M ⧸ N
def

additiveHomToMultiplicativeHom

L87 ↗
LocalClassFieldTheory.additiveHomToMultiplicativeHom
Documentation

Multiplicative form of an additive homomorphism, kept polymorphic for the same elaboration reason as additiveEquivToQuotientHom.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def additiveHomToMultiplicativeHom
    {G B : Type} [Group G] [AddCommGroup B]
    (f : Additive G →+ B) : G →* Multiplicative B
def

multiplicativeQuotientGroup

L96 ↗
LocalClassFieldTheory.multiplicativeQuotientGroup
Documentation

The multiplicative group structure on an additive submodule quotient. This is passed explicitly at concrete call sites to avoid rediscovering it by unfolding the coefficient representation.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def multiplicativeQuotientGroup
    {M : Type} [AddCommGroup M] (N : Submodule ℤ M) :
    Group (Multiplicative (M ⧸ N))
def

kernelOfAdditiveQuotientHom

L103 ↗
LocalClassFieldTheory.kernelOfAdditiveQuotientHom
Documentation

Kernel of a homomorphism into a multiplicative additive quotient, with the codomain structure supplied directly.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def kernelOfAdditiveQuotientHom
    {G M : Type} [Group G] [AddCommGroup M]
    (N : Submodule ℤ M) (f : G →* Multiplicative (M ⧸ N)) : Subgroup G
def

quotientMulEquivOfSurjectiveAdditiveQuotient

L111 ↗
LocalClassFieldTheory.quotientMulEquivOfSurjectiveAdditiveQuotient
Documentation

First-isomorphism-theorem comparison for a surjection onto a multiplicative additive quotient.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def quotientMulEquivOfSurjectiveAdditiveQuotient
    {G M : Type} [CommGroup G] [AddCommGroup M]
    (N : Submodule ℤ M) (S : Subgroup G)
    (f : G →* Multiplicative (M ⧸ N))
    (hker : kernelOfAdditiveQuotientHom N f = S)
    (hsurj : Function.Surjective f) :
    G ⧸ S ≃* Multiplicative (M ⧸ N)
def

mulEquivMultiplicativeToEquiv

L125 ↗
LocalClassFieldTheory.mulEquivMultiplicativeToEquiv
Documentation

Forget the type tags in an equivalence whose codomain is the multiplicative form of an additive group.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · full declaration
def mulEquivMultiplicativeToEquiv
    {G B : Type} [Group G] [AddCommGroup B]
    (e : G ≃* Multiplicative B) : G ≃ B where
  toFun q := Multiplicative.toAdd (e q)
  invFun q := e.symm (Multiplicative.ofAdd q)
  left_inv q := e.left_inv q
  right_inv q := e.right_inv (Multiplicative.ofAdd q)
def

additiveFixedUnitToInvariantsNormQuotientHom

L134 ↗
LocalClassFieldTheory.additiveFixedUnitToInvariantsNormQuotientHom
Documentation

Additive quotient map from fixed units to invariant units modulo norms.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def additiveFixedUnitToInvariantsNormQuotientHom
    [Fintype (Gal(L/K))] :
    Additive (fixedSubgroup (Gal(L / K)) Lˣ) →+
      (unitsInvariantSubmodule K L ⧸ unitsTateH0NormSubmodule K L)
def

fixedUnitToInvariantsNormQuotientMonoidHom

L142 ↗
LocalClassFieldTheory.fixedUnitToInvariantsNormQuotientMonoidHom
Documentation

Send a fixed unit to its invariant-unit class modulo norms.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def fixedUnitToInvariantsNormQuotientMonoidHom
    [Fintype (Gal(L/K))] :
    fixedSubgroup (Gal(L / K)) Lˣ →*
      Multiplicative
        (unitsInvariantSubmodule K L ⧸ unitsTateH0NormSubmodule K L)
theorem

fixedUnitToInvariantsNormQuotientMonoidHom_apply

L152 ↗
LocalClassFieldTheory.fixedUnitToInvariantsNormQuotientMonoidHom_apply
Documentation

A fixed unit maps to its canonical invariant-unit class modulo norms.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem fixedUnitToInvariantsNormQuotientMonoidHom_apply
    [Fintype (Gal(L/K))] (x : fixedSubgroup (Gal(L/K)) Lˣ) :
    Multiplicative.toAdd
        (fixedUnitToInvariantsNormQuotientMonoidHom K L x) =
      (unitsTateH0NormSubmodule K L).mkQ
        (additiveFixedUnitsEquivInvariants K L (Additive.ofMul x))
theorem

fixedUnitToInvariantsNormQuotientMonoidHom_ker

L162 ↗
LocalClassFieldTheory.fixedUnitToInvariantsNormQuotientMonoidHom_ker
Documentation

The kernel of the fixed-unit quotient map is exactly the Herbrand norm subgroup inside the fixed subgroup.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem fixedUnitToInvariantsNormQuotientMonoidHom_ker
    [Fintype (Gal(L/K))] :
    kernelOfAdditiveQuotientHom (unitsTateH0NormSubmodule K L)
        (fixedUnitToInvariantsNormQuotientMonoidHom K L) =
      (tateNormSubgroup (Gal(L / K)) Lˣ).subgroupOf
        (fixedSubgroup (Gal(L / K)) Lˣ)
theorem

fixedUnitToInvariantsNormQuotientMonoidHom_surjective

L208 ↗
LocalClassFieldTheory.fixedUnitToInvariantsNormQuotientMonoidHom_surjective
Documentation

Every invariant-unit class modulo norms has a multiplicatively fixed representative.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem fixedUnitToInvariantsNormQuotientMonoidHom_surjective
    [Fintype (Gal(L/K))] :
    Function.Surjective (fixedUnitToInvariantsNormQuotientMonoidHom K L)
def

herbrandH0MulEquivInvariantsNormQuotient

L231 ↗
LocalClassFieldTheory.herbrandH0MulEquivInvariantsNormQuotient
Documentation

The multiplicative Herbrand quotient is the invariant-unit quotient by norms.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def herbrandH0MulEquivInvariantsNormQuotient
    [Fintype (Gal(L/K))]
def

herbrandH0EquivTateCohomologyZero

L243 ↗
LocalClassFieldTheory.herbrandH0EquivTateCohomologyZero
Documentation

The multiplicative Herbrand quotient of field units is mathlib's degree-zero Tate cohomology.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def herbrandH0EquivTateCohomologyZero [Fintype (Gal(L/K))] :
    HerbrandH0 (Gal(L / K)) Lˣ ≃
      tateCohomology (Rep.ofAlgebraAutOnUnits K L) 0
theorem

cardinalMk_herbrandH0_fieldUnits_eq_tateCohomology_zero

L252 ↗
LocalClassFieldTheory.cardinalMk_herbrandH0_fieldUnits_eq_tateCohomology_zero
Documentation

Cardinality transport from the concrete Herbrand quotient to mathlib's degree-zero Tate cohomology.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem cardinalMk_herbrandH0_fieldUnits_eq_tateCohomology_zero
    [Fintype (Gal(L/K))] :
    Cardinal.mk (HerbrandH0 (Gal(L / K)) Lˣ) =
      Cardinal.mk (tateCohomology (Rep.ofAlgebraAutOnUnits K L) 0)
theorem

unitsRhoSub_toMul_eq_sigmaMinusOne

L260 ↗
LocalClassFieldTheory.unitsRhoSub_toMul_eq_sigmaMinusOne
Documentation

Subtraction by the identity in the actual unit representation is the multiplicative coboundary x ↦ g•x/x.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem unitsRhoSub_toMul_eq_sigmaMinusOne
    (g : Gal(L/K)) (x : Lˣ) :
    (Additive.toMul ((Rep.ofAlgebraAutOnUnits K L).ρ g (Additive.ofMul x)) : Lˣ) * x⁻¹ =
      sigmaMinusOne (Gal(L / K)) Lˣ g x
def

additiveNormKernelEquivUnitsNormKer

L268 ↗
LocalClassFieldTheory.additiveNormKernelEquivUnitsNormKer
Documentation

Multiplicative norm-one units and the kernel of the norm on the actual unit representation are the same additive group.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · full declaration
def additiveNormKernelEquivUnitsNormKer [Fintype (Gal(L/K))] :
    Additive (normKernelSubgroup (Gal(L / K)) Lˣ) ≃+
      LinearMap.ker (unitsNormLinearMap K L) where
  toFun x := ⟨Additive.ofMul
      ((Additive.toMul x : normKernelSubgroup (Gal(L / K)) Lˣ) : Lˣ), by
    apply Additive.toMul.injective
    change Additive.toMul
      (unitsNormLinearMap K L (Additive.ofMul
        ((Additive.toMul x : normKernelSubgroup (Gal(L / K)) Lˣ) : Lˣ))) = 1
    rw [unitsNormLinearMap_toMul_eq_tateNorm K L
      ((Additive.toMul x : normKernelSubgroup (Gal(L / K)) Lˣ) : Lˣ)]
    exact (Additive.toMul x).property⟩
  invFun x := Additive.ofMul ⟨Additive.toMul (x : Additive Lˣ), by
    change tateNorm (Gal(L / K)) Lˣ (Additive.toMul (x : Additive Lˣ)) = 1
    rw [← unitsNormLinearMap_toMul_eq_tateNorm K L
      (Additive.toMul (x : Additive Lˣ))]
    have hx := congrArg Additive.toMul x.property
    exact hx⟩
  left_inv x := rfl
  right_inv x := rfl
  map_add' x y := rfl
def

unitsRhoSubToNormKerLinearMap

L292 ↗
LocalClassFieldTheory.unitsRhoSubToNormKerLinearMap
Documentation

The actual additive differential ρ(g)-1, with codomain restricted to the kernel of the norm.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def unitsRhoSubToNormKerLinearMap [Fintype (Gal(L/K))]
    (g : Gal(L/K)) :
    Additive Lˣ →ₗ[ℤ] LinearMap.ker (unitsNormLinearMap K L)
def

additiveNormKernelToUnitsBoundaryQuotientHom

L311 ↗
LocalClassFieldTheory.additiveNormKernelToUnitsBoundaryQuotientHom
Documentation

Additive quotient map from the multiplicative norm kernel to the standard boundary presentation of degree-minus-one Tate cohomology.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def additiveNormKernelToUnitsBoundaryQuotientHom
    [Fintype (Gal(L/K))] (g : Gal(L/K)) :
    Additive (normKernelSubgroup (Gal(L / K)) Lˣ) →+
      LinearMap.ker (unitsNormLinearMap K L) ⧸
        LinearMap.range (unitsRhoSubToNormKerLinearMap K L g)
def

normKernelToUnitsBoundaryQuotientMonoidHom

L321 ↗
LocalClassFieldTheory.normKernelToUnitsBoundaryQuotientMonoidHom
Documentation

Multiplicative form of the standard boundary quotient map.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def normKernelToUnitsBoundaryQuotientMonoidHom
    [Fintype (Gal(L/K))] (g : Gal(L/K)) :
    normKernelSubgroup (Gal(L / K)) Lˣ →*
      Multiplicative
        (LinearMap.ker (unitsNormLinearMap K L) ⧸
          LinearMap.range (unitsRhoSubToNormKerLinearMap K L g))
theorem

normKernelToUnitsBoundaryQuotientMonoidHom_ker

L332 ↗
LocalClassFieldTheory.normKernelToUnitsBoundaryQuotientMonoidHom_ker
Documentation

The kernel of the standard boundary quotient map is the augmentation subgroup generated by ρ(g)-1.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem normKernelToUnitsBoundaryQuotientMonoidHom_ker
    [Fintype (Gal(L/K))] (g : Gal(L/K)) :
    kernelOfAdditiveQuotientHom
        (LinearMap.range (unitsRhoSubToNormKerLinearMap K L g))
        (normKernelToUnitsBoundaryQuotientMonoidHom K L g) =
      (augmentationSubgroup (Gal(L / K)) Lˣ g).subgroupOf
        (normKernelSubgroup (Gal(L / K)) Lˣ)
theorem

normKernelToUnitsBoundaryQuotientMonoidHom_surjective

L389 ↗
LocalClassFieldTheory.normKernelToUnitsBoundaryQuotientMonoidHom_surjective
Documentation

Every class of the standard boundary quotient has a representative in the multiplicative norm kernel.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem normKernelToUnitsBoundaryQuotientMonoidHom_surjective
    [Fintype (Gal(L/K))] (g : Gal(L/K)) :
    Function.Surjective
      (normKernelToUnitsBoundaryQuotientMonoidHom K L g)
def

herbrandHminusOneMulEquivUnitsBoundaryQuotient

L416 ↗
LocalClassFieldTheory.herbrandHminusOneMulEquivUnitsBoundaryQuotient
Documentation

The multiplicative Herbrand quotient is the standard additive boundary quotient used by mathlib's finite-cyclic Tate complex.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def herbrandHminusOneMulEquivUnitsBoundaryQuotient
    [Fintype (Gal(L/K))] (g : Gal(L/K)) :
    HerbrandHMinusOne (Gal(L / K)) Lˣ g ≃*
      Multiplicative
        (LinearMap.ker (unitsNormLinearMap K L) ⧸
          LinearMap.range (unitsRhoSubToNormKerLinearMap K L g))
def

herbrandHminusOneEquivUnitsBoundaryQuotient

L432 ↗
LocalClassFieldTheory.herbrandHminusOneEquivUnitsBoundaryQuotient
Documentation

Type-level comparison with the standard boundary quotient.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def herbrandHminusOneEquivUnitsBoundaryQuotient
    [Fintype (Gal(L/K))] (g : Gal(L/K)) :
    HerbrandHMinusOne (Gal(L / K)) Lˣ g ≃
      LinearMap.ker (unitsNormLinearMap K L) ⧸
        LinearMap.range (unitsRhoSubToNormKerLinearMap K L g)
def

unitsTateHminusOneIsoBoundaryQuotient

L442 ↗
LocalClassFieldTheory.unitsTateHminusOneIsoBoundaryQuotient
Documentation

Mathlib's degree-minus-one Tate object is its standard finite-cyclic boundary quotient ker N / im(ρ(g)-1).

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def unitsTateHminusOneIsoBoundaryQuotient
    [FiniteDimensional K L] (g : Gal(L/K))
    (hg : ∀ x : Gal(L / K), x ∈ Subgroup.zpowers g) :
    tateCohomology (Rep.ofAlgebraAutOnUnits K L) (-1) ≅
      ModuleCat.of ℤ
        (LinearMap.ker (unitsNormLinearMap K L) ⧸
          LinearMap.range (unitsRhoSubToNormKerLinearMap K L g))
def

herbrandHminusOneEquivUnitsTateHminusOne

L472 ↗
LocalClassFieldTheory.herbrandHminusOneEquivUnitsTateHminusOne
Documentation

Genuine comparison of the multiplicative H⁻¹ quotient for field units with Mathlib's actual Tate H⁻¹ object.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
def herbrandHminusOneEquivUnitsTateHminusOne
    [FiniteDimensional K L] (g : Gal(L/K))
    (hg : ∀ x : Gal(L / K), x ∈ Subgroup.zpowers g) :
    HerbrandHMinusOne (Gal(L / K)) Lˣ g ≃
      tateCohomology (Rep.ofAlgebraAutOnUnits K L) (-1)
theorem

cardinalMk_herbrandHminusOne_fieldUnits_eq_unitsTateHminusOne

L483 ↗
LocalClassFieldTheory.cardinalMk_herbrandHminusOne_fieldUnits_eq_unitsTateHminusOne
Documentation

Cardinality transport from the concrete Herbrand H⁻¹ quotient to the actual Tate H⁻¹ object. The statement is valid without introducing an extraneous finiteness hypothesis.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology
noncomputable section
open scoped BigOperators
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CategoryTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem cardinalMk_herbrandHminusOne_fieldUnits_eq_unitsTateHminusOne
    [FiniteDimensional K L] (g : Gal(L/K))
    (hg : ∀ x : Gal(L / K), x ∈ Subgroup.zpowers g) :
    Cardinal.mk (HerbrandHMinusOne (Gal(L / K)) Lˣ g) =
      Cardinal.mk (tateCohomology (Rep.ofAlgebraAutOnUnits K L) (-1))

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