Tensoring a short exact sequence of representations

Tensoring with a fixed representation M is right exact, but not exact in general. This file records that a short exact sequence of representations which is split as a sequence of k-modules stays short exact after tensoring on the left with M: the k-linear retraction of the first map survives tensoring and keeps the tensored first map injective, while right exactness of the tensor product supplies exactness and the surjectivity of the last map. The dimension-shifting sequences through the modules induced and coinduced from the trivial subgroup are of this kind. Tensoring with a representation whose underlying module is flat over k preserves every short exact sequence.

Main statements

• Rep.exact_iff_function_exact: a short complex of representations is exact if and only if the underlying linear maps form an exact pair.
• Rep.exists_leftInverse_of_rightInverse, Rep.exists_rightInverse_of_leftInverse: a short exact sequence of representations has a k-linear retraction of its first map exactly when it has a k-linear section of its last map.
• Rep.shortExact_map_tensorLeft_of_injective: tensoring on the left preserves a short exact sequence as soon as the tensored first map stays injective.
• Rep.shortExact_map_tensorLeft_of_flat: tensoring on the left with a representation whose underlying module is flat preserves every short exact sequence.
• Rep.leftInverse_whiskerLeft: tensoring on the left keeps a k-linear retraction.
• Rep.shortExact_map_tensorLeft_of_leftInverse, Rep.shortExact_map_tensorLeft_of_rightInverse: tensoring on the left preserves a short exact sequence whose first map has a k-linear retraction, or whose last map has a k-linear section.
• Rep.shortExact_map_tensorRight_of_injective: tensoring on the right preserves a short exact sequence as soon as the tensored first map stays injective.
• Rep.shortExact_map_tensorRight_of_flat, Rep.shortExact_map_tensorRight_of_leftInverse, Rep.shortExact_map_tensorRight_of_rightInverse: the same for tensoring on the right, through the braiding.

theorem Rep.exact_iff_function_exact {k : Type u} {G : Type v} [Monoid G] [Ring k] (S : CategoryTheory.ShortComplex (Rep k G)) : S.Exact ↔ Function.Exact ⇑(Hom.hom S.f) ⇑(Hom.hom S.g)

A short complex of representations is exact if and only if the underlying linear maps form an exact pair.

theorem Rep.exists_leftInverse_of_rightInverse {k : Type u} {G : Type v} [Monoid G] [Ring k] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.Exact) [CategoryTheory.Mono S.f] {s : ↑S.X₃ →ₗ[k] ↑S.X₂} (hs : Function.RightInverse ⇑s ⇑(Hom.hom S.g)) : ∃ (r : ↑S.X₂ →ₗ[k] ↑S.X₁), Function.LeftInverse ⇑r ⇑(Hom.hom S.f)

In a short exact sequence of representations, a k-linear section of the last map gives a k-linear retraction of the first map.

theorem Rep.exists_rightInverse_of_leftInverse {k : Type u} {G : Type v} [Monoid G] [Ring k] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.Exact) [CategoryTheory.Epi S.g] {r : ↑S.X₂ →ₗ[k] ↑S.X₁} (hr : Function.LeftInverse ⇑r ⇑(Hom.hom S.f)) : ∃ (s : ↑S.X₃ →ₗ[k] ↑S.X₂), Function.RightInverse ⇑s ⇑(Hom.hom S.g)

In a short exact sequence of representations, a k-linear retraction of the first map gives a k-linear section of the last map.

theorem Rep.shortExact_map_tensorLeft_of_injective {k : Type u} {G : Type v} [Monoid G] [CommRing k] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.Exact) [CategoryTheory.Epi S.g] (M : Rep k G) (hf : Function.Injective ⇑(LinearMap.lTensor (↑M) (Hom.hom S.f).toLinearMap)) : (S.map (CategoryTheory.MonoidalCategory.tensorLeft M)).ShortExact

Tensoring on the left with M sends an exact sequence ending in an epimorphism to a short exact sequence when the tensored first map is injective.

theorem Rep.shortExact_map_tensorLeft_of_flat {k : Type u} {G : Type v} [Monoid G] [CommRing k] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.ShortExact) (M : Rep k G) [Module.Flat k ↑M] : (S.map (CategoryTheory.MonoidalCategory.tensorLeft M)).ShortExact

Tensoring on the left with a representation whose underlying module is flat over k preserves short exact sequences.

theorem Rep.leftInverse_whiskerLeft {k : Type u} {G : Type v} [Monoid G] [CommRing k] (M : Rep k G) {A B : Rep k G} (f : A ⟶ B) {r : ↑B →ₗ[k] ↑A} (hr : Function.LeftInverse ⇑r ⇑(Hom.hom f)) : Function.LeftInverse ⇑(LinearMap.lTensor (↑M) r) ⇑(Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f))

Tensoring on the left with M keeps a k-linear retraction r of a morphism of representations: M ⊗ r is a retraction of M ◁ f.

theorem Rep.shortExact_map_tensorLeft_of_leftInverse {k : Type u} {G : Type v} [Monoid G] [CommRing k] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.Exact) [CategoryTheory.Epi S.g] (M : Rep k G) {r : ↑S.X₂ →ₗ[k] ↑S.X₁} (hr : Function.LeftInverse ⇑r ⇑(Hom.hom S.f)) : (S.map (CategoryTheory.MonoidalCategory.tensorLeft M)).ShortExact

Tensoring on the left with M sends an exact sequence ending in an epimorphism to a short exact sequence if the first map has a k-linear retraction.

theorem Rep.shortExact_map_tensorLeft_of_rightInverse {k : Type u} {G : Type v} [Monoid G] [CommRing k] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.Exact) [CategoryTheory.Mono S.f] (M : Rep k G) {s : ↑S.X₃ →ₗ[k] ↑S.X₂} (hs : Function.RightInverse ⇑s ⇑(Hom.hom S.g)) : (S.map (CategoryTheory.MonoidalCategory.tensorLeft M)).ShortExact

Tensoring on the left with M sends an exact sequence starting in a monomorphism to a short exact sequence if the last map has a k-linear section.

theorem Rep.shortExact_map_tensorRight_of_injective {k : Type u} {G : Type v} [Monoid G] [CommRing k] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.Exact) [CategoryTheory.Epi S.g] (M : Rep k G) (hf : Function.Injective ⇑(LinearMap.rTensor (↑M) (Hom.hom S.f).toLinearMap)) : (S.map (CategoryTheory.MonoidalCategory.tensorRight M)).ShortExact

Tensoring on the right with M sends an exact sequence ending in an epimorphism to a short exact sequence when the tensored first map is injective.

theorem Rep.shortExact_map_tensorRight_of_leftInverse {k : Type u} {G : Type v} [Monoid G] [CommRing k] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.Exact) [CategoryTheory.Epi S.g] (M : Rep k G) {r : ↑S.X₂ →ₗ[k] ↑S.X₁} (hr : Function.LeftInverse ⇑r ⇑(Hom.hom S.f)) : (S.map (CategoryTheory.MonoidalCategory.tensorRight M)).ShortExact

Tensoring on the right with M sends an exact sequence ending in an epimorphism to a short exact sequence if the first map has a k-linear retraction.

theorem Rep.shortExact_map_tensorRight_of_rightInverse {k : Type u} {G : Type v} [Monoid G] [CommRing k] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.Exact) [CategoryTheory.Mono S.f] (M : Rep k G) {s : ↑S.X₃ →ₗ[k] ↑S.X₂} (hs : Function.RightInverse ⇑s ⇑(Hom.hom S.g)) : (S.map (CategoryTheory.MonoidalCategory.tensorRight M)).ShortExact

Tensoring on the right with M sends an exact sequence starting in a monomorphism to a short exact sequence if the last map has a k-linear section.

theorem Rep.shortExact_map_tensorRight_of_flat {k : Type u} {G : Type v} [Monoid G] [CommRing k] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.ShortExact) (M : Rep k G) [Module.Flat k ↑M] : (S.map (CategoryTheory.MonoidalCategory.tensorRight M)).ShortExact

Tensoring on the right with a representation whose underlying module is flat over k preserves short exact sequences.