The dimension-shifting sequences

For a representation A of a group G, the embedding A ⟶ Coind_⊥^G A into the representation coinduced from the trivial subgroup and the projection Ind_⊥^G A ⟶ A from the induced representation give short exact sequences

0 ⟶ A ⟶ Coind_⊥^G A ⟶ dimensionShiftUp A ⟶ 0 and 0 ⟶ dimensionShiftDown A ⟶ Ind_⊥^G A ⟶ A ⟶ 0,

which stay short exact after restriction along any monoid homomorphism H →* G. As representations of G itself, the middle terms have vanishing positive-degree cohomology (groupCohomology.isZero_coindBot_succ), respectively homology (groupHomology.isZero_indBot_succ), and for a finite group vanishing Tate cohomology in every degree (TauCeti.TateCohomology.isZero_coindBot, TauCeti.TateCohomology.isZero_indBot), so the connecting homomorphisms of these sequences shift degrees. This is the dimension shifting of Milne, Class Field Theory, II 1.13 and 1.28; this file provides the sequences themselves.

The constructions follow ClassFieldTheory/Cohomology/Functors/UpDown.lean in kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509.

Main definitions

• Rep.dimensionShiftUp, Rep.dimensionShiftUpπ, Rep.dimensionShiftUpSES: the cokernel of A ⟶ Coind_⊥^G A and its short complex.
• Rep.dimensionShiftDown, Rep.dimensionShiftDownι, Rep.dimensionShiftDownSES: the kernel of Ind_⊥^G A ⟶ A and its short complex.
• Rep.dimensionShiftUpπIsCokernel, Rep.dimensionShiftDownιIsKernel: their universal properties. The definitions are opaque, so consumers construct maps through these properties.
• Rep.dimensionShiftUpMap, Rep.dimensionShiftDownMap: the maps a morphism of coefficients induces on the two shifts, and Rep.dimensionShiftUpSESMap, Rep.dimensionShiftDownSESMap: the morphisms it induces between the short complexes.
• Rep.dimensionShiftUpFunctor, Rep.dimensionShiftDownFunctor: the two shifts as endofunctors of Rep k G, with the natural transformations Rep.dimensionShiftUpπNatTrans and Rep.dimensionShiftDownιNatTrans, and Rep.dimensionShiftUpSESFunctor, Rep.dimensionShiftDownSESFunctor: the two sequences as functors to short complexes.

Main statements

• Rep.dimensionShiftUpSES_def, Rep.dimensionShiftDownSES_def: the maps in the two short complexes.
• Rep.dimensionShiftUpSES_shortExact, Rep.dimensionShiftUpSES_res_shortExact, Rep.dimensionShiftUpSES_tensorLeft_shortExact: the upward sequence is short exact, also after restriction and after tensoring on the left with any representation.
• Rep.dimensionShiftDownSES_shortExact, Rep.dimensionShiftDownSES_res_shortExact, Rep.dimensionShiftDownSES_tensorLeft_shortExact: the same for the downward sequence.
• Rep.dimensionShiftUpπ_naturality, Rep.dimensionShiftDownι_naturality: the coefficient maps commute with the quotient projection and with the kernel inclusion.

References

• J. S. Milne, Class Field Theory, Chapter II, §1.
• K. S. Brown, Cohomology of Groups, Chapter III, §7.

The upward dimension shift

noncomputable def Rep.dimensionShiftUp {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : Rep.{u, u, u} k G

The cokernel of the embedding A ⟶ Coind_⊥^G A, so that Hⁿ⁺¹(G, dimensionShiftUp A) ≅ Hⁿ⁺²(G, A).

Equations

• A.dimensionShiftUp = CategoryTheory.Limits.cokernel A.coindBotUnit

noncomputable def Rep.dimensionShiftUpπ {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : coindBot k G ↑A ⟶ A.dimensionShiftUp

The projection from the coinduced module onto dimensionShiftUp A.

Equations

• A.dimensionShiftUpπ = CategoryTheory.Limits.cokernel.π A.coindBotUnit

instance Rep.dimensionShiftUpπ_epi {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : CategoryTheory.Epi A.dimensionShiftUpπ

The projection onto dimensionShiftUp A is an epimorphism.

@[simp]

theorem Rep.coindBotUnit_comp_dimensionShiftUpπ {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : CategoryTheory.CategoryStruct.comp A.coindBotUnit A.dimensionShiftUpπ = 0

The embedding into the coinduced module followed by the dimension-shift projection is zero.

@[simp]

theorem Rep.coindBotUnit_comp_dimensionShiftUpπ_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) {Z : Rep.{u, u, u} k G} (h : A.dimensionShiftUp ⟶ Z) : CategoryTheory.CategoryStruct.comp A.coindBotUnit (CategoryTheory.CategoryStruct.comp A.dimensionShiftUpπ h) = CategoryTheory.CategoryStruct.comp 0 h

The embedding into the coinduced module followed by the dimension-shift projection is zero.

noncomputable def Rep.dimensionShiftUpπIsCokernel {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ A.dimensionShiftUpπ ⋯)

The dimension-shift projection is a cokernel of the embedding into the coinduced module.

Equations

• A.dimensionShiftUpπIsCokernel = CategoryTheory.Limits.cokernelIsCokernel A.coindBotUnit

noncomputable def Rep.dimensionShiftUpSES {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)

The short complex A ⟶ Coind_⊥^G A ⟶ dimensionShiftUp A.

Equations

• A.dimensionShiftUpSES = CategoryTheory.ShortComplex.cokernelSequence A.coindBotUnit

theorem Rep.dimensionShiftUpSES_def {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : A.dimensionShiftUpSES = { X₁ := A, X₂ := coindBot k G ↑A, X₃ := A.dimensionShiftUp, f := A.coindBotUnit, g := A.dimensionShiftUpπ, zero := ⋯ }

The upward dimension-shifting short complex has maps the embedding into the coinduced module and the dimension-shift projection.

@[simp]

theorem Rep.dimensionShiftUpSES_X₁ {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : A.dimensionShiftUpSES.X₁ = A

The first object in the upward dimension-shifting short complex is A.

@[simp]

theorem Rep.dimensionShiftUpSES_X₂ {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : A.dimensionShiftUpSES.X₂ = coindBot k G ↑A

The middle object in the upward dimension-shifting short complex is coinduced from ⊥.

@[simp]

theorem Rep.dimensionShiftUpSES_X₃ {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : A.dimensionShiftUpSES.X₃ = A.dimensionShiftUp

The last object in the upward dimension-shifting short complex is dimensionShiftUp A.

theorem Rep.dimensionShiftUpSES_shortExact {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : A.dimensionShiftUpSES.ShortExact

The short complex A ⟶ Coind_⊥^G A ⟶ dimensionShiftUp A is short exact.

theorem Rep.dimensionShiftUpSES_res_shortExact {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) {H : Type u_1} [Monoid H] (f : H →* G) : (A.dimensionShiftUpSES.map (resFunctor f)).ShortExact

The upward dimension-shifting short complex stays short exact after restriction along any monoid homomorphism f : H →* G.

theorem Rep.dimensionShiftUpSES_tensorLeft_shortExact {k G : Type u} [CommRing k] [Group G] (A M : Rep.{u, u, u} k G) : (A.dimensionShiftUpSES.map (CategoryTheory.MonoidalCategory.tensorLeft M)).ShortExact

The upward dimension-shifting short complex stays short exact after tensoring on the left with any representation M: the embedding into the coinduced module has the k-linear retraction f ↦ f 1.

The downward dimension shift

noncomputable def Rep.dimensionShiftDown {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : Rep.{u, u, u} k G

The kernel of the projection Ind_⊥^G A ⟶ A, so that Ĥⁿ(G, A) ≅ Ĥⁿ⁺¹(G, dimensionShiftDown A) when G is finite.

Equations

• A.dimensionShiftDown = CategoryTheory.Limits.kernel A.indBotCounit

noncomputable def Rep.dimensionShiftDownι {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : A.dimensionShiftDown ⟶ indBot k G ↑A

The inclusion of dimensionShiftDown A into the induced module.

Equations

• A.dimensionShiftDownι = CategoryTheory.Limits.kernel.ι A.indBotCounit

instance Rep.dimensionShiftDownι_mono {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : CategoryTheory.Mono A.dimensionShiftDownι

The inclusion of dimensionShiftDown A is a monomorphism.

@[simp]

theorem Rep.dimensionShiftDownι_comp_indBotCounit {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : CategoryTheory.CategoryStruct.comp A.dimensionShiftDownι A.indBotCounit = 0

The dimension-shift inclusion followed by the projection onto A is zero.

@[simp]

theorem Rep.dimensionShiftDownι_comp_indBotCounit_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) {Z : Rep.{u, u, u} k G} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp A.dimensionShiftDownι (CategoryTheory.CategoryStruct.comp A.indBotCounit h) = CategoryTheory.CategoryStruct.comp 0 h

The dimension-shift inclusion followed by the projection onto A is zero.

noncomputable def Rep.dimensionShiftDownιIsKernel {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι A.dimensionShiftDownι ⋯)

The dimension-shift inclusion is a kernel of the projection onto A.

Equations

• A.dimensionShiftDownιIsKernel = CategoryTheory.Limits.kernelIsKernel A.indBotCounit

noncomputable def Rep.dimensionShiftDownSES {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)

The short complex dimensionShiftDown A ⟶ Ind_⊥^G A ⟶ A.

Equations

• A.dimensionShiftDownSES = CategoryTheory.ShortComplex.kernelSequence A.indBotCounit

theorem Rep.dimensionShiftDownSES_def {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : A.dimensionShiftDownSES = { X₁ := A.dimensionShiftDown, X₂ := indBot k G ↑A, X₃ := A, f := A.dimensionShiftDownι, g := A.indBotCounit, zero := ⋯ }

The downward dimension-shifting short complex has maps the dimension-shift inclusion and the projection onto A.

@[simp]

theorem Rep.dimensionShiftDownSES_X₁ {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : A.dimensionShiftDownSES.X₁ = A.dimensionShiftDown

The first object in the downward dimension-shifting short complex is dimensionShiftDown A.

@[simp]

theorem Rep.dimensionShiftDownSES_X₂ {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : A.dimensionShiftDownSES.X₂ = indBot k G ↑A

The middle object in the downward dimension-shifting short complex is induced from ⊥.

@[simp]

theorem Rep.dimensionShiftDownSES_X₃ {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : A.dimensionShiftDownSES.X₃ = A

The last object in the downward dimension-shifting short complex is A.

theorem Rep.dimensionShiftDownSES_shortExact {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : A.dimensionShiftDownSES.ShortExact

The short complex dimensionShiftDown A ⟶ Ind_⊥^G A ⟶ A is short exact.

theorem Rep.dimensionShiftDownSES_res_shortExact {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) {H : Type u_1} [Monoid H] (f : H →* G) : (A.dimensionShiftDownSES.map (resFunctor f)).ShortExact

The downward dimension-shifting short complex stays short exact after restriction along any monoid homomorphism f : H →* G.

theorem Rep.dimensionShiftDownSES_tensorLeft_shortExact {k G : Type u} [CommRing k] [Group G] (A M : Rep.{u, u, u} k G) : (A.dimensionShiftDownSES.map (CategoryTheory.MonoidalCategory.tensorLeft M)).ShortExact

The downward dimension-shifting short complex stays short exact after tensoring on the left with any representation M: the projection from the induced module has the k-linear section a ↦ ⟦1 ⊗ₜ a⟧.

Functoriality of the dimension-shifting sequences

noncomputable def Rep.dimensionShiftUpMap {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : A.dimensionShiftUp ⟶ B.dimensionShiftUp

The morphism induced on the upward dimension shift by a representation morphism.

Equations

• Rep.dimensionShiftUpMap f = CategoryTheory.Limits.cokernel.map A.coindBotUnit B.coindBotUnit f (Rep.coindBotMap f) ⋯

@[simp]

theorem Rep.dimensionShiftUpπ_naturality {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp A.dimensionShiftUpπ (dimensionShiftUpMap f) = CategoryTheory.CategoryStruct.comp (coindBotMap f) B.dimensionShiftUpπ

The map on upward shifts commutes with their quotient projections.

@[simp]

theorem Rep.dimensionShiftUpπ_naturality_assoc {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) {Z : Rep.{u, u, u} k G} (h : B.dimensionShiftUp ⟶ Z) : CategoryTheory.CategoryStruct.comp A.dimensionShiftUpπ (CategoryTheory.CategoryStruct.comp (dimensionShiftUpMap f) h) = CategoryTheory.CategoryStruct.comp (coindBotMap f) (CategoryTheory.CategoryStruct.comp B.dimensionShiftUpπ h)

The map on upward shifts commutes with their quotient projections.

@[simp]

theorem Rep.dimensionShiftUpMap_id {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : dimensionShiftUpMap (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id A.dimensionShiftUp

The upward shift map preserves identity morphisms.

@[simp]

theorem Rep.dimensionShiftUpMap_comp {k G : Type u} [CommRing k] [Group G] {A B C : Rep.{u, u, u} k G} (f : A ⟶ B) (g : B ⟶ C) : dimensionShiftUpMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (dimensionShiftUpMap f) (dimensionShiftUpMap g)

The upward shift map preserves composition.

noncomputable def Rep.dimensionShiftUpSESMap {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : { X₁ := A, X₂ := coindBot k G ↑A, X₃ := A.dimensionShiftUp, f := A.coindBotUnit, g := A.dimensionShiftUpπ, zero := ⋯ } ⟶ { X₁ := B, X₂ := coindBot k G ↑B, X₃ := B.dimensionShiftUp, f := B.coindBotUnit, g := B.dimensionShiftUpπ, zero := ⋯ }

A coefficient morphism induces a morphism of the public presentations of the upward dimension-shifting sequences (dimensionShiftUpSES_def).

Equations

• Rep.dimensionShiftUpSESMap f = { τ₁ := f, τ₂ := Rep.coindBotMap f, τ₃ := Rep.dimensionShiftUpMap f, comm₁₂ := ⋯, comm₂₃ := ⋯ }

@[simp]

theorem Rep.dimensionShiftUpSESMap_τ₁ {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : (dimensionShiftUpSESMap f).τ₁ = f

The first component of the upward sequence morphism.

@[simp]

theorem Rep.dimensionShiftUpSESMap_τ₂ {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : (dimensionShiftUpSESMap f).τ₂ = coindBotMap f

The middle component of the upward sequence morphism.

@[simp]

theorem Rep.dimensionShiftUpSESMap_τ₃ {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : (dimensionShiftUpSESMap f).τ₃ = dimensionShiftUpMap f

The last component of the upward sequence morphism.

noncomputable def Rep.dimensionShiftDownMap {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : A.dimensionShiftDown ⟶ B.dimensionShiftDown

The morphism induced on the downward dimension shift by a representation morphism.

Equations

• Rep.dimensionShiftDownMap f = CategoryTheory.Limits.kernel.map A.indBotCounit B.indBotCounit (Rep.indBotMap f) f ⋯

@[simp]

theorem Rep.dimensionShiftDownι_naturality {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (dimensionShiftDownMap f) B.dimensionShiftDownι = CategoryTheory.CategoryStruct.comp A.dimensionShiftDownι (indBotMap f)

The map on downward shifts commutes with their inclusions into induced modules.

@[simp]

theorem Rep.dimensionShiftDownι_naturality_assoc {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) {Z : Rep.{u, u, u} k G} (h : indBot k G ↑B ⟶ Z) : CategoryTheory.CategoryStruct.comp (dimensionShiftDownMap f) (CategoryTheory.CategoryStruct.comp B.dimensionShiftDownι h) = CategoryTheory.CategoryStruct.comp A.dimensionShiftDownι (CategoryTheory.CategoryStruct.comp (indBotMap f) h)

The map on downward shifts commutes with their inclusions into induced modules.

@[simp]

theorem Rep.dimensionShiftDownMap_id {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : dimensionShiftDownMap (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id A.dimensionShiftDown

The downward shift map preserves identity morphisms.

@[simp]

theorem Rep.dimensionShiftDownMap_comp {k G : Type u} [CommRing k] [Group G] {A B C : Rep.{u, u, u} k G} (f : A ⟶ B) (g : B ⟶ C) : dimensionShiftDownMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (dimensionShiftDownMap f) (dimensionShiftDownMap g)

The downward shift map preserves composition.

noncomputable def Rep.dimensionShiftDownSESMap {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : { X₁ := A.dimensionShiftDown, X₂ := indBot k G ↑A, X₃ := A, f := A.dimensionShiftDownι, g := A.indBotCounit, zero := ⋯ } ⟶ { X₁ := B.dimensionShiftDown, X₂ := indBot k G ↑B, X₃ := B, f := B.dimensionShiftDownι, g := B.indBotCounit, zero := ⋯ }

A coefficient morphism induces a morphism of the public presentations of the downward dimension-shifting sequences (dimensionShiftDownSES_def).

Equations

• Rep.dimensionShiftDownSESMap f = { τ₁ := Rep.dimensionShiftDownMap f, τ₂ := Rep.indBotMap f, τ₃ := f, comm₁₂ := ⋯, comm₂₃ := ⋯ }

@[simp]

theorem Rep.dimensionShiftDownSESMap_τ₁ {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : (dimensionShiftDownSESMap f).τ₁ = dimensionShiftDownMap f

The first component of the downward sequence morphism.

@[simp]

theorem Rep.dimensionShiftDownSESMap_τ₂ {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : (dimensionShiftDownSESMap f).τ₂ = indBotMap f

The middle component of the downward sequence morphism.

@[simp]

theorem Rep.dimensionShiftDownSESMap_τ₃ {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : (dimensionShiftDownSESMap f).τ₃ = f

The last component of the downward sequence morphism.

Bundled coefficient functoriality

noncomputable def Rep.dimensionShiftUpFunctor {k G : Type u} [CommRing k] [Group G] : CategoryTheory.Functor (Rep.{u, u, u} k G) (Rep.{u, u, u} k G)

The upward dimension shift as an endofunctor on representations.

Equations

• Rep.dimensionShiftUpFunctor = { obj := Rep.dimensionShiftUp, map := fun {X Y : Rep.{?u.1, ?u.1, ?u.1} k G} (f : X ⟶ Y) => Rep.dimensionShiftUpMap f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem Rep.dimensionShiftUpFunctor_obj {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : dimensionShiftUpFunctor.obj A = A.dimensionShiftUp

The upward shift functor evaluates to the upward shift.

@[simp]

theorem Rep.dimensionShiftUpFunctor_map {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : dimensionShiftUpFunctor.map f = dimensionShiftUpMap f

The upward shift functor acts on morphisms by dimensionShiftUpMap.

noncomputable def Rep.dimensionShiftUpπNatTrans {k G : Type u} [CommRing k] [Group G] : coindBotRepFunctor ⟶ dimensionShiftUpFunctor

The projection from coinduction to the upward shift, natural in coefficients.

Equations

• Rep.dimensionShiftUpπNatTrans = { app := fun (A : Rep.{?u.1, ?u.1, ?u.1} k G) => A.dimensionShiftUpπ, naturality := ⋯ }

@[simp]

theorem Rep.dimensionShiftUpπNatTrans_app {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : dimensionShiftUpπNatTrans.app A = A.dimensionShiftUpπ

The component of the upward projection is the cokernel projection.

noncomputable def Rep.dimensionShiftUpSESFunctor {k G : Type u} [CommRing k] [Group G] : CategoryTheory.Functor (Rep.{u, u, u} k G) (CategoryTheory.ShortComplex (Rep.{u, u, u} k G))

The upward short exact sequence as a functor of coefficient representations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Rep.dimensionShiftUpSESFunctor_obj {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : dimensionShiftUpSESFunctor.obj A = A.dimensionShiftUpSES

The upward sequence functor evaluates to the upward short exact sequence.

@[simp]

theorem Rep.dimensionShiftUpSESFunctor_map {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : dimensionShiftUpSESFunctor.map f = dimensionShiftUpSESMap f

The upward sequence functor acts on morphisms by dimensionShiftUpSESMap.

noncomputable def Rep.dimensionShiftDownFunctor {k G : Type u} [CommRing k] [Group G] : CategoryTheory.Functor (Rep.{u, u, u} k G) (Rep.{u, u, u} k G)

The downward dimension shift as an endofunctor on representations.

Equations

• Rep.dimensionShiftDownFunctor = { obj := Rep.dimensionShiftDown, map := fun {X Y : Rep.{?u.1, ?u.1, ?u.1} k G} (f : X ⟶ Y) => Rep.dimensionShiftDownMap f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem Rep.dimensionShiftDownFunctor_obj {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : dimensionShiftDownFunctor.obj A = A.dimensionShiftDown

The downward shift functor evaluates to the downward shift.

@[simp]

theorem Rep.dimensionShiftDownFunctor_map {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : dimensionShiftDownFunctor.map f = dimensionShiftDownMap f

The downward shift functor acts on morphisms by dimensionShiftDownMap.

noncomputable def Rep.dimensionShiftDownιNatTrans {k G : Type u} [CommRing k] [Group G] : dimensionShiftDownFunctor ⟶ indBotRepFunctor

The inclusion of the downward shift into induction, natural in coefficients.

Equations

• Rep.dimensionShiftDownιNatTrans = { app := fun (A : Rep.{?u.1, ?u.1, ?u.1} k G) => A.dimensionShiftDownι, naturality := ⋯ }

@[simp]

theorem Rep.dimensionShiftDownιNatTrans_app {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : dimensionShiftDownιNatTrans.app A = A.dimensionShiftDownι

The component of the downward inclusion is the kernel inclusion.

noncomputable def Rep.dimensionShiftDownSESFunctor {k G : Type u} [CommRing k] [Group G] : CategoryTheory.Functor (Rep.{u, u, u} k G) (CategoryTheory.ShortComplex (Rep.{u, u, u} k G))

The downward short exact sequence as a functor of coefficient representations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Rep.dimensionShiftDownSESFunctor_obj {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) : dimensionShiftDownSESFunctor.obj A = A.dimensionShiftDownSES

The downward sequence functor evaluates to the downward short exact sequence.

@[simp]

theorem Rep.dimensionShiftDownSESFunctor_map {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : dimensionShiftDownSESFunctor.map f = dimensionShiftDownSESMap f

The downward sequence functor acts on morphisms by dimensionShiftDownSESMap.