Module

Core.lean

Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.Core

5 declarations indexed from sourceView source ↗

Module documentation

Low-degree Herbrand quotients

The foundational constructions and their comparison with mathlib Tate cohomology are split into focused modules. This public module retains the Herbrand quotient and its multiplicativity result.

Imports2

Imported by4

def

herbrandQuotient

L37 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient

Documentation

Herbrand-quotient theory the Herbrand-quotient definition: the Herbrand quotient of the actual low-degree multiplicative Tate quotients. The finiteness assumptions prevent Nat.card from silently taking the value 0 on infinite quotients.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · statement

def herbrandQuotient (σ : G)
    [Finite (HerbrandH0 G A)] [Finite (HerbrandHMinusOne G A σ)] : ℚ

theorem

herbrandQuotient_eq_card_ratio

L42 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient_eq_card_ratio

Documentation

The Herbrand quotient is definitionally the ratio #H⁰ / #H^{-1}.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · statement

theorem herbrandQuotient_eq_card_ratio (σ : G)
    [Finite (HerbrandH0 G A)] [Finite (HerbrandHMinusOne G A σ)] :
    herbrandQuotient (G := G) (A := A) σ =
      (Nat.card (HerbrandH0 G A) : ℚ) /
        (Nat.card (HerbrandHMinusOne G A σ) : ℚ)

theorem

herbrandQuotient_eq_one_of_card_eq

L51 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient_eq_one_of_card_eq

Documentation

If the actual low-degree quotients have the same finite cardinality, then the Herbrand quotient is 1.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · statement

theorem herbrandQuotient_eq_one_of_card_eq (σ : G)
    [Finite (HerbrandH0 G A)] [Finite (HerbrandHMinusOne G A σ)]
    (hcard : Nat.card (HerbrandH0 G A) = Nat.card (HerbrandHMinusOne G A σ)) :
    herbrandQuotient (G := G) (A := A) σ = 1

theorem

herbrandQuotient_finite_module_eq_one

L63 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient_finite_module_eq_one

Documentation

Herbrand-quotient theory Herbrand-quotient multiplicativity: the Herbrand quotient of a finite cyclic module is 1.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · statement

theorem herbrandQuotient_finite_module_eq_one
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) [Finite A] :
    herbrandQuotient (G := G) (A := A) σ = 1

theorem

herbrandQuotient_exact_multiplicative

L73 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient_exact_multiplicative

Documentation

Herbrand-quotient theory Herbrand-quotient multiplicativity: Herbrand quotient multiplicativity for a short exact sequence of multiplicative G-modules, proved from the standard two-periodic Tate complex and mathlib's homology long exact sequence.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · statement

theorem herbrandQuotient_exact_multiplicative
    {G A B C : Type}
    [Group G] [Fintype G]
    [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C]
    (i : A →* B) (j : B →* C)
    (hi : ∀ (g : G) (a : A), i (g • a) = g • i a)
    (hj : ∀ (g : G) (b : B), j (g • b) = g • j b)
    (hker : ∀ b : B, j b = 1 ↔ ∃ a : A, i a = b)
    (hinj : Function.Injective i)
    (hsurj : ∀ c : C, ∃ b : B, j b = c) (σ : G)
    (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    [Finite (HerbrandH0 G A)] [Finite (HerbrandHMinusOne G A σ)]
    [Finite (HerbrandH0 G B)] [Finite (HerbrandHMinusOne G B σ)]
    [Finite (HerbrandH0 G C)] [Finite (HerbrandHMinusOne G C σ)] :
    herbrandQuotient (G := G) (A := B) σ =
      herbrandQuotient (G := G) (A := A) σ *
        herbrandQuotient (G := G) (A := C) σ

Module documentation

Low-degree Herbrand quotients

Declarations

herbrandQuotient

herbrandQuotient_eq_card_ratio

herbrandQuotient_eq_one_of_card_eq

herbrandQuotient_finite_module_eq_one

herbrandQuotient_exact_multiplicative