Module

Index.lean

Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.Index

4 declarations indexed from sourceView source ↗

Module documentation

Cardinal consequences of a Herbrand quotient

This file isolates the elementary cardinal arithmetic at the end of the low-degree Herbrand quotient calculation. If a finite low-degree Tate quotient has Herbrand quotient equal to a natural number n, then its degree-zero cardinality is n times its negative-first cardinality. In particular the degree-zero cardinality is at least n.

Imports1

Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandFiniteness

Imported by2

theorem

herbrandH0_card_eq_mul_herbrandHMinusOne_card

L35 ↗

CyclicCohomology.herbrandH0_card_eq_mul_herbrandHMinusOne_card

Documentation

Clearing the nonzero denominator in a Herbrand quotient whose value is a natural number.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} {A : Type uA}
    [Group G] [Fintype G]
    [CommGroup A] [MulDistribMulAction G A]

Lean source · statement

theorem herbrandH0_card_eq_mul_herbrandHMinusOne_card
    (σ : G) (n : ℕ)
    [Finite (HerbrandH0 G A)]
    [Finite (HerbrandHMinusOne G A σ)]
    (hquotient :
      herbrandQuotient (G := G) (A := A) σ = n) :
    Nat.card (HerbrandH0 G A) =
      n * Nat.card
        (HerbrandHMinusOne G A σ)

theorem

le_herbrandH0_card_of_herbrandQuotient_eq_nat

L61 ↗

CyclicCohomology.le_herbrandH0_card_of_herbrandQuotient_eq_nat

Documentation

Cardinal-arithmetic step for low-degree Herbrand cohomology: a natural-valued Herbrand quotient is a lower bound for the degree-zero Tate quotient.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} {A : Type uA}
    [Group G] [Fintype G]
    [CommGroup A] [MulDistribMulAction G A]

Lean source · statement

theorem le_herbrandH0_card_of_herbrandQuotient_eq_nat
    (σ : G) (n : ℕ)
    [Finite (HerbrandH0 G A)]
    [Finite (HerbrandHMinusOne G A σ)]
    (hquotient :
      herbrandQuotient (G := G) (A := A) σ = n) :
    n ≤ Nat.card (HerbrandH0 G A)

theorem

lowDegree_card_eq_of_herbrandQuotient_eq_nat_of_le

L82 ↗

CyclicCohomology.lowDegree_card_eq_of_herbrandQuotient_eq_nat_of_le

Documentation

If the degree-zero cardinality is also bounded above by the natural value of the Herbrand quotient, both low-degree cardinalities are forced: #H⁰ = n and #H⁻¹ = 1.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} {A : Type uA}
    [Group G] [Fintype G]
    [CommGroup A] [MulDistribMulAction G A]

Lean source · statement

theorem lowDegree_card_eq_of_herbrandQuotient_eq_nat_of_le
    (σ : G) (n : ℕ) (hn : 0 < n)
    [Finite (HerbrandH0 G A)]
    [Finite (HerbrandHMinusOne G A σ)]
    (hquotient :
      herbrandQuotient (G := G) (A := A) σ = n)
    (hle : Nat.card (HerbrandH0 G A) ≤ n) :
    Nat.card (HerbrandH0 G A) = n ∧
      Nat.card (HerbrandHMinusOne G A σ) = 1

theorem

herbrandHMinusOne_subsingleton_of_herbrandQuotient_eq_nat_of_le

L110 ↗

CyclicCohomology.herbrandHMinusOne_subsingleton_of_herbrandQuotient_eq_nat_of_le

Documentation

Subsingleton form of the negative-first conclusion.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} {A : Type uA}
    [Group G] [Fintype G]
    [CommGroup A] [MulDistribMulAction G A]

Lean source · statement

theorem herbrandHMinusOne_subsingleton_of_herbrandQuotient_eq_nat_of_le
    (σ : G) (n : ℕ) (hn : 0 < n)
    [Finite (HerbrandH0 G A)]
    [Finite (HerbrandHMinusOne G A σ)]
    (hquotient :
      herbrandQuotient (G := G) (A := A) σ = n)
    (hle : Nat.card (HerbrandH0 G A) ≤ n) :
    Subsingleton (HerbrandHMinusOne G A σ)

Module documentation

Cardinal consequences of a Herbrand quotient

Declarations

herbrandH0_card_eq_mul_herbrandHMinusOne_card

le_herbrandH0_card_of_herbrandQuotient_eq_nat

lowDegree_card_eq_of_herbrandQuotient_eq_nat_of_le

herbrandHMinusOne_subsingleton_of_herbrandQuotient_eq_nat_of_le