Tate cohomology and the Herbrand quotient

TheoremPeriodicity of Tate cohomology for finite cyclic groups#✓fully proved

Let \(R\) be a commutative ring, \(G\) a finite cyclic group and \(A\) a representation of \(G\) over \(R\). Then for every integer \(n\), the Tate cohomology groups \(\hat{H}^n(G, A)\) and \(\hat{H}^{n+2}(G, A)\) are isomorphic as \(R\)-modules.

theorem nonempty_periodicityIso {R G : Type u} [CommRing R] [Group G]
    [Fintype G] [IsCyclic G] (A : Rep R G) (n : ℤ) :
    Nonempty (tateCohomology A n ≅ tateCohomology A (n + 2))

DefinitionCardinality of Tate cohomology#✓fully proved

Let \(G\) be a finite group, \(R\) a commutative ring, \(M\) an \(R\)-linear representation of \(G\) and \(n\) an integer. This is the cardinality of the Tate cohomology group \(\hat H^n(G, M)\), as a cardinal number (possibly infinite).

noncomputable def tateCohomologyCard (M : Rep R G) (n : ℤ) : Cardinal :=
  Cardinal.mk ↥(tateCohomology M n)

Used by 3

Used byCardinality of finite Tate cohomology as a natural number · Cardinality of Tate homology · Cardinality of Tate homology in degree zero

DefinitionCardinality of Tate homology#✓fully proved

Let \(G\) be a finite group, \(R\) a commutative ring and \(M\) an \(R\)-linear representation of \(G\). For an integer \(n\), the cardinality \(h_n(M)\) of the degree-\(n\) Tate homology of \(M\) is defined as the cardinal number of the Tate cohomology group \(\hat H^{-n-1}(G, M)\), following the convention \(\hat H_n = \hat H^{-n-1}\).

noncomputable def tateHomologyCard (M : Rep R G) (n : ℤ) : Cardinal :=
  tateCohomologyCard M (-n - 1)

Uses 1 · Used by 1

Statement usesCardinality of Tate cohomology

Used byCardinality of Tate homology in degree zero

TheoremCardinality of Tate homology in degree zero#✓fully proved

Let \(G\) be a finite group, \(R\) a commutative ring and \(M\) an \(R\)-linear representation of \(G\). The cardinality of the degree-\(0\) Tate homology of \(M\) equals the cardinality of the Tate cohomology group \(\hat H^{-1}(G, M)\).

The cardinality of Tate homology in degree \(n\) is defined as that of \(\hat H^{-n-1}(G, M)\), so this holds by definition.

@[simp] theorem tateHomologyCard_zero (M : Rep R G) :
    tateHomologyCard M 0 = tateCohomologyCard M (-1)

Uses 2

Statement usesCardinality of Tate cohomology · Cardinality of Tate homology

TheoremCardinality of finite Tate cohomology as a natural number#✓fully proved

Let \(G\) be a finite group, \(R\) a commutative ring, \(M\) an \(R\)-linear representation of \(G\) and \(n\) an integer such that the Tate cohomology group \(\hat H^n(G, M)\) is finite. Then the cardinality of \(\hat H^n(G, M)\) equals its number of elements, a natural number viewed as a cardinal number.

theorem tateCohomologyCard_eq_natCast (M : Rep R G) (n : ℤ)
    [Finite ↥(tateCohomology M n)] :
    tateCohomologyCard M n = Nat.card ↥(tateCohomology M n)

Uses 1

Statement usesCardinality of Tate cohomology

DefinitionFiniteness hypothesis for the Herbrand quotient#✓fully proved

Let \(G\) be a finite group, \(R\) a commutative ring and \(M\) an \(R\)-linear representation of \(G\). The representation \(M\) satisfies the Herbrand finiteness hypothesis when its Tate cohomology groups \(\hat H^0(G, M)\) and \(\hat H^{-1}(G, M)\) are both finite.

def HerbrandFinite (M : Rep R G) : Prop :=
  Finite ↥(tateCohomology M 0) ∧ Finite ↥(tateCohomology M (-1))

Used by 6

Used byHerbrand quotient · Herbrand quotients agree when Tate cohomology in degrees \(0\) and \(-1\) is in bijection · The denominator of the Herbrand quotient is nonzero · The denominator of the Herbrand quotient is positive · Herbrand quotient as a ratio of orders · Positivity of the Herbrand quotient

DefinitionHerbrand quotient#✓fully proved

Let \(G\) be a finite group, \(R\) a commutative ring and \(M\) an \(R\)-linear representation of \(G\) whose Tate cohomology groups \(\hat H^0(G, M)\) and \(\hat H^{-1}(G, M)\) are finite. The Herbrand quotient of \(M\) is the rational number \(h(M) = |\hat H^0(G, M)| / |\hat H^{-1}(G, M)|\), where \(|X|\) is the number of elements of \(X\).

noncomputable def herbrandQuotient (M : Rep R G) (h : HerbrandFinite M) : ℚ :=
  haveI := h.1
  haveI := h.2
  (Nat.card ↥(tateCohomology M 0) : ℚ) / Nat.card ↥(tateCohomology M (-1))

Uses 1 · Used by 3

Statement usesFiniteness hypothesis for the Herbrand quotient

Used byHerbrand quotients agree when Tate cohomology in degrees \(0\) and \(-1\) is in bijection · Herbrand quotient as a ratio of orders · Positivity of the Herbrand quotient

TheoremHerbrand quotient as a ratio of orders#✓fully proved

Let \(G\) be a finite group, \(R\) a commutative ring and \(M\) an \(R\)-linear representation of \(G\) whose Tate cohomology groups \(\hat H^0(G, M)\) and \(\hat H^{-1}(G, M)\) are finite. Then the Herbrand quotient of \(M\) equals the rational number \(|\hat H^0(G, M)| / |\hat H^{-1}(G, M)|\), where \(|X|\) is the number of elements of \(X\).

theorem herbrandQuotient_eq (M : Rep R G) (h : HerbrandFinite M) :
    herbrandQuotient M h = (Nat.card ↥(tateCohomology M 0) : ℚ) /
      Nat.card ↥(tateCohomology M (-1))

Uses 2 · Used by 2

Statement usesFiniteness hypothesis for the Herbrand quotient · Herbrand quotient

Used byHerbrand quotients agree when Tate cohomology in degrees \(0\) and \(-1\) is in bijection · Positivity of the Herbrand quotient

TheoremThe denominator of the Herbrand quotient is positive#✓fully proved

Let \(G\) be a finite group, \(R\) a commutative ring and \(M\) an \(R\)-linear representation of \(G\) whose Tate cohomology groups \(\hat H^0(G, M)\) and \(\hat H^{-1}(G, M)\) are finite. Then the number of elements of \(\hat H^{-1}(G, M)\) is positive.

theorem herbrandQuotient_den_pos (M : Rep R G) (h : HerbrandFinite M) :
    0 < Nat.card ↥(tateCohomology M (-1))

Uses 1 · Used by 1

Statement usesFiniteness hypothesis for the Herbrand quotient

Used byThe denominator of the Herbrand quotient is nonzero

TheoremThe denominator of the Herbrand quotient is nonzero#✓fully proved

Let \(G\) be a finite group, \(R\) a commutative ring and \(M\) an \(R\)-linear representation of \(G\) whose Tate cohomology groups \(\hat H^0(G, M)\) and \(\hat H^{-1}(G, M)\) are finite. Then the number of elements of \(\hat H^{-1}(G, M)\) is nonzero.

theorem herbrandQuotient_den_ne_zero (M : Rep R G) (h : HerbrandFinite M) :
    Nat.card ↥(tateCohomology M (-1)) ≠ 0

Uses 2

Statement usesFiniteness hypothesis for the Herbrand quotient

Proof usesThe denominator of the Herbrand quotient is positive

TheoremPositivity of the Herbrand quotient#✓fully proved

Let \(G\) be a finite group, \(R\) a commutative ring and \(M\) an \(R\)-linear representation of \(G\) whose Tate cohomology groups \(\hat H^0(G, M)\) and \(\hat H^{-1}(G, M)\) are finite. Then the Herbrand quotient of \(M\) is strictly positive.

theorem herbrandQuotient_pos (M : Rep R G) (h : HerbrandFinite M) :
    0 < herbrandQuotient M h

Uses 3

Statement usesFiniteness hypothesis for the Herbrand quotient · Herbrand quotient

Proof usesHerbrand quotient as a ratio of orders

TheoremHerbrand quotients agree when Tate cohomology in degrees \(0\) and \(-1\) is in bijection#✓fully proved

Let \(G\) be a finite group, \(R\) a commutative ring and \(M\), \(N\) two \(R\)-linear representations of \(G\) whose Tate cohomology groups \(\hat H^0(G, M)\), \(\hat H^{-1}(G, M)\), \(\hat H^0(G, N)\) and \(\hat H^{-1}(G, N)\) are finite. If there are bijections between the underlying sets of \(\hat H^0(G, M)\) and \(\hat H^0(G, N)\) and between those of \(\hat H^{-1}(G, M)\) and \(\hat H^{-1}(G, N)\), then the Herbrand quotients of \(M\) and \(N\) are equal.

theorem herbrandQuotient_congr {M N : Rep R G} {hM : HerbrandFinite M}
    {hN : HerbrandFinite N}
    (e₀ : ↥(tateCohomology M 0) ≃ ↥(tateCohomology N 0))
    (e₁ : ↥(tateCohomology M (-1)) ≃ ↥(tateCohomology N (-1))) :
    herbrandQuotient M hM = herbrandQuotient N hN

Uses 3

Statement usesFiniteness hypothesis for the Herbrand quotient · Herbrand quotient

Proof usesHerbrand quotient as a ratio of orders

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.