Documentation

TauCeti.RepresentationTheory.Homological.GroupCohomology.DimensionShift

Dimension shifting in ordinary group cohomology #

For a representation A of a group G, the upward dimension-shifting sequence

0 ⟶ A ⟶ Coind_⊥^G A ⟶ dimensionShiftUp A ⟶ 0

has a middle term whose cohomology vanishes in every positive degree (Shapiro's lemma). Its connecting homomorphism is therefore an isomorphism Hⁿ⁺¹(G, dimensionShiftUp A) ≅ Hⁿ⁺²(G, A), and surjective in the remaining degree H⁰(G, dimensionShiftUp A) ⟶ H¹(G, A). The same holds after restriction to any subgroup, so a vanishing hypothesis can be moved between degrees simultaneously on all subgroups, which is what the inflation-restriction sequence needs.

Only the upward sequence appears here. The downward sequence has Ind_⊥^G A as its middle term, which is acyclic for ordinary cohomology only when G is finite; the downward shift is therefore stated for Tate cohomology instead, in TauCeti.TateCohomology.dimensionShiftDownIso.

Each isomorphism below has Mathlib's groupCohomology.δ as its forward map, so its naturality is the existing naturality of δ and no abstract choice of isomorphism enters.

Main definitions #

Main statements #

References #

source
noncomputable def TauCeti.groupCohomology.dimensionShiftUpIso {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (n : ℕ) :
groupCohomology A.dimensionShiftUp (n + 1) ≅ groupCohomology A (n + 2)

Dimension shifting as an isomorphism: Hⁿ⁺¹(G, dimensionShiftUp A) ≅ Hⁿ⁺²(G, A), the connecting homomorphism of the coinduced sequence, whose middle term has vanishing cohomology in both degrees (Shapiro's lemma). The forward map is Mathlib's δ, so naturality is free; degree 0 is only an epimorphism, hence the indexing starts at n + 1.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.groupCohomology.dimensionShiftUpIso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (n : ℕ) :
    (dimensionShiftUpIso A n).hom = groupCohomology.δ ⋯ (n + 1) (n + 2) ⋯

    The dimension-shifting isomorphism is the connecting homomorphism.

    source
    @[simp]
    theorem TauCeti.groupCohomology.isZero_dimensionShiftUp_iff {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (n : ℕ) :
    CategoryTheory.Limits.IsZero (groupCohomology A.dimensionShiftUp (n + 1)) ↔ CategoryTheory.Limits.IsZero (groupCohomology A (n + 2))

    Vanishing in degree n + 1 of an upward shift is vanishing in degree n + 2 of the original module. This is the form in which the shift is consumed: it moves a vanishing hypothesis between degrees.

    source
    theorem TauCeti.groupCohomology.epi_δ_dimensionShiftUp_zero {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) :
    CategoryTheory.Epi (groupCohomology.δ ⋯ 0 1 ⋯)

    In the remaining degree the connecting homomorphism H⁰(G, dimensionShiftUp A) ⟶ H¹(G, A) is surjective: Shapiro's lemma only gives vanishing of the coinduced middle term in positive degrees, so degree 0 has the input an epimorphism needs but not the second input an isomorphism would need.

    source
    noncomputable def TauCeti.groupCohomology.dimensionShiftUpResIso {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) (n : ℕ) :
    groupCohomology (Rep.res S.subtype A.dimensionShiftUp) (n + 1) ≅ groupCohomology (Rep.res S.subtype A) (n + 2)

    Dimension shifting after restriction to a subgroup, as an isomorphism: Hⁿ⁺¹(S, dimensionShiftUp A) ≅ Hⁿ⁺²(S, A). The forward map is Mathlib's δ, so naturality is free; degree 0 is only an epimorphism, hence the indexing starts at n + 1.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.groupCohomology.dimensionShiftUpResIso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) (n : ℕ) :
      (dimensionShiftUpResIso A S n).hom = groupCohomology.δ ⋯ (n + 1) (n + 2) ⋯

      The restricted dimension-shifting isomorphism is the connecting homomorphism.

      source
      @[simp]
      theorem TauCeti.groupCohomology.isZero_res_dimensionShiftUp_iff {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) (n : ℕ) :
      CategoryTheory.Limits.IsZero (groupCohomology (Rep.res S.subtype A.dimensionShiftUp) (n + 1)) ↔ CategoryTheory.Limits.IsZero (groupCohomology (Rep.res S.subtype A) (n + 2))

      After restriction to a subgroup, vanishing in degree n + 1 of an upward shift is vanishing in degree n + 2 of the original module. Together with the unrestricted form this moves a vanishing hypothesis between degrees simultaneously on every subgroup.

      source
      theorem TauCeti.groupCohomology.epi_δ_res_dimensionShiftUp_zero {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) :
      CategoryTheory.Epi (groupCohomology.δ ⋯ 0 1 ⋯)

      After restriction to a subgroup, the connecting homomorphism H⁰(S, dimensionShiftUp A) ⟶ H¹(S, A) is surjective: Shapiro's lemma only gives vanishing of the coinduced middle term in positive degrees, so degree 0 has the input an epimorphism needs but not the second input an isomorphism would need.