Coinduction: exactness and coextension of scalars

Coinduction along a subgroup preserves short exact sequences of representations. Unlike coinduction along an arbitrary homomorphism, subgroup coinduction preserves epimorphisms; together with its right adjoint structure this gives exactness, without a finite-index assumption. This allows connecting maps to be compared through Shapiro's isomorphism.

On the module side, coinduction along a monoid homomorphism φ : H →* G is coextension of scalars along MonoidAlgebra.mapDomainRingHom k φ : k[H] →+* k[G]: the k[G]-module Hom_{k[H]}(k[G], V) of Mathlib's ModuleCat.coextendScalars is isomorphic to the module of Mathlib's coinduced representation Representation.coind φ ρ, by evaluation at the monoid elements (Representation.coextendScalarsEquivCoind). This transports statements about coextension of scalars on module categories, such as its action on Grothendieck groups of group algebras, to coinduced and induced representations.

Mathlib's coinduced action is evaluated by Representation.coind_apply_coe_apply: (h • f) h₁ = f (h₁ * h).

References

• K. S. Brown, Cohomology of Groups, Chapter III, §6 and §9.

instance Rep.instAdditiveCoindFunctor_tauCeti {R : Type u} [CommRing R] {G : Type v} {H : Type w} [Monoid G] [Monoid H] (φ : H →* G) : (coindFunctor R φ).Additive

Coinduction acts additively on coefficient maps.

instance Rep.instPreservesHomologySubtypeMemSubgroupCoindFunctorSubtype_tauCeti {R : Type u} [CommRing R] {G : Type v} [Group G] (H : Subgroup G) : (coindFunctor R H.subtype).PreservesHomology

Subgroup coinduction preserves homology of short complexes of representations.

instance Rep.instPreservesFiniteColimitsSubtypeMemSubgroupCoindFunctorSubtype_tauCeti {R : Type u} [CommRing R] {G : Type v} [Group G] (H : Subgroup G) : CategoryTheory.Limits.PreservesFiniteColimits (coindFunctor R H.subtype)

Subgroup coinduction is exact, so also preserves finite colimits.

theorem Representation.coind_apply_coe_apply {k : Type u_1} {G : Type u_2} {H : Type u_3} {V : Type u_4} [Semiring k] [Monoid G] [Monoid H] [AddCommMonoid V] [Module k V] (φ : G →* H) (ρ : Representation k G V) (f : ↥(coindV φ ρ)) (h h₁ : H) : ↑(((coind φ ρ) h) f) h₁ = ↑f (h₁ * h)

The coinduced action translates the argument of a function: (h • f) h₁ = f (h₁ * h).

@[simp]

theorem Representation.coind'_asAlgebraHom_hom_apply {k : Type u} {H : Type w} {G : Type v} [CommRing k] [Monoid H] [Monoid G] (φ : H →* G) (A : Rep.{max u v, u, w} k H) (r : MonoidAlgebra k G) (f : Rep.res φ (Rep.leftRegular k G) ⟶ A) (a : MonoidAlgebra k G) : (Rep.Hom.hom (((coind' φ A).asAlgebraHom r) f)) a = (Rep.Hom.hom f) (a * r)

k[G] acts on the coinduced representation Representation.coind' φ A, whose elements are the morphisms Rep.res φ (Rep.leftRegular k G) ⟶ A, by right multiplication on the source k[G].

noncomputable def Representation.coextendScalarsEquivCoind {k : Type u} {H : Type w} {G : Type v} [CommRing k] [Monoid H] [Monoid G] (φ : H →* G) {V : Type (max u v)} [AddCommGroup V] [Module k V] (ρ : Representation k H V) : ↑((ModuleCat.coextendScalars (MonoidAlgebra.mapDomainRingHom k φ)).obj ↧ρ.asModule) ≃ₗ[MonoidAlgebra k G] (coind φ ρ).asModule

Coinduction is coextension of scalars. For a monoid homomorphism φ : H →* G and a representation ρ of H on V, the k[G]-module Hom_{k[H]}(k[G], V), with k[H] acting on k[G] through φ, is isomorphic to the module of Mathlib's coinduced representation Representation.coind φ ρ: a homomorphism x corresponds to the function g ↦ x (single g 1). It is Mathlib's Rep.coindIso read through the identification of k[H]-linear maps k[G] → V with the morphisms of Rep.coind' φ.

Equations

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

@[simp]

theorem Representation.coextendScalarsEquivCoind_apply {k : Type u} {H : Type w} {G : Type v} [CommRing k] [Monoid H] [Monoid G] (φ : H →* G) {V : Type (max u v)} [AddCommGroup V] [Module k V] (ρ : Representation k H V) (x : ↑((ModuleCat.coextendScalars (MonoidAlgebra.mapDomainRingHom k φ)).obj ↧ρ.asModule)) (g : G) : ↑((coextendScalarsEquivCoind φ ρ) x) g = ((ModuleCat.CoextendScalars.equiv (MonoidAlgebra.mapDomainRingHom k φ) ↧ρ.asModule) x) (MonoidAlgebra.single g 1)

Representation.coextendScalarsEquivCoind evaluates a homomorphism at the monoid elements.

@[simp]

theorem Representation.coextendScalarsEquivCoind_symm_apply_single {k : Type u} {H : Type w} {G : Type v} [CommRing k] [Monoid H] [Monoid G] (φ : H →* G) {V : Type (max u v)} [AddCommGroup V] [Module k V] (ρ : Representation k H V) (y : (coind φ ρ).asModule) (g : G) : ((ModuleCat.CoextendScalars.equiv (MonoidAlgebra.mapDomainRingHom k φ) ↧ρ.asModule) ((coextendScalarsEquivCoind φ ρ).symm y)) (MonoidAlgebra.single g 1) = ↑y g

The inverse of Representation.coextendScalarsEquivCoind sends a coinduced function y to the homomorphism taking the value y g at single g 1.