Free summands of free mixed modules

Over an algebra whose unit is a scalar, the free-module functor is full and faithful on the mixed sums of copies of the tensor unit and of an odd line, idempotent endomorphisms of those mixed sums split off further mixed sums, and consequently a direct summand of a free mixed module is again a free mixed module.

Idempotent complex matrices split

theorem RS.exists_split_of_linear_idem {n : ℕ} (f : (Fin n → ℂ) →ₗ[ℂ] Fin n → ℂ) (hf : f ∘ₗ f = f) : ∃ (r : ℕ) (s : (Fin r → ℂ) →ₗ[ℂ] Fin n → ℂ) (t : (Fin n → ℂ) →ₗ[ℂ] Fin r → ℂ), s ∘ₗ t = f ∧ t ∘ₗ s = LinearMap.id

An idempotent endomorphism of a finite-dimensional coordinate space factors through a smaller coordinate space.

theorem RS.exists_split_of_matrix_idem {n : ℕ} (M : Matrix (Fin n) (Fin n) ℂ) (hM : M * M = M) : ∃ (r : ℕ) (S : Matrix (Fin n) (Fin r) ℂ) (T : Matrix (Fin r) (Fin n) ℂ), S * T = M ∧ T * S = 1

An idempotent complex square matrix splits through a rectangular pair of matrices.

Matrix calculus for biproducts

theorem RS.components_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {J K M : Type} [Finite J] [Fintype K] [Finite M] {f : J → D} {g : K → D} {h : M → D} (x : ⨁ f ⟶ ⨁ g) (y : ⨁ g ⟶ ⨁ h) (j : J) (m : M) : CategoryTheory.Limits.biproduct.components (CategoryTheory.CategoryStruct.comp x y) j m = ∑ k : K, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.components x j k) (CategoryTheory.Limits.biproduct.components y k m)

The matrix of a composite is the product of the matrices.

theorem RS.hom_ext_components {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {J K : Type} [Finite J] [Finite K] {f : J → D} {g : K → D} (x y : ⨁ f ⟶ ⨁ g) (h : ∀ (j : J) (k : K), CategoryTheory.Limits.biproduct.components x j k = CategoryTheory.Limits.biproduct.components y j k) : x = y

Two maps of biproducts with the same matrix agree.

theorem RS.components_id_self {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {J : Type} [Finite J] {f : J → D} (j : J) : CategoryTheory.Limits.biproduct.components (CategoryTheory.CategoryStruct.id (⨁ f)) j j = CategoryTheory.CategoryStruct.id (f j)

The diagonal entries of the identity matrix.

theorem RS.components_id_ne {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {J : Type} [Finite J] {f : J → D} {j k : J} (h : j ≠ k) : CategoryTheory.Limits.biproduct.components (CategoryTheory.CategoryStruct.id (⨁ f)) j k = 0

The off-diagonal entries of the identity matrix vanish.

Whiskering by the odd line is injective on morphisms

noncomputable def RS.OddLine.rot {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (X : D) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X L.obj) L.obj ≅ X

Whiskering an object twice by the line returns the object.

Equations

• L.rot X = CategoryTheory.MonoidalCategoryStruct.associator X L.obj L.obj ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso X L.sq ≪≫ CategoryTheory.MonoidalCategoryStruct.rightUnitor X

theorem RS.OddLine.rot_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (X : D) : (L.rot X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X L.obj L.obj).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X L.sq.hom) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)

theorem RS.OddLine.whiskerRight_rot {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) {X Y : D} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f L.obj) L.obj) (L.rot Y).hom = CategoryTheory.CategoryStruct.comp (L.rot X).hom f

Whiskering a morphism twice by the line conjugates it.

theorem RS.OddLine.whiskerRight_rot_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) {X Y : D} (f : X ⟶ Y) {Z : D} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f L.obj) L.obj) (CategoryTheory.CategoryStruct.comp (L.rot Y).hom h) = CategoryTheory.CategoryStruct.comp (L.rot X).hom (CategoryTheory.CategoryStruct.comp f h)

Whiskering a morphism twice by the line conjugates it.

theorem RS.OddLine.whiskerRight_whiskerRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) {X Y : D} (f : X ⟶ Y) : CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f L.obj) L.obj = CategoryTheory.CategoryStruct.comp (L.rot X).hom (CategoryTheory.CategoryStruct.comp f (L.rot Y).inv)

theorem RS.OddLine.rot_whiskerRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) {X Y : D} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (L.rot X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f L.obj) L.obj) (L.rot Y).hom) = f

Double whiskering by the line is undone by the rotation.

theorem RS.OddLine.whiskerRight_injective {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) {X Y : D} : Function.Injective fun (f : X ⟶ Y) => CategoryTheory.MonoidalCategoryStruct.whiskerRight f L.obj

Whiskering by the odd line is injective on morphisms.

theorem RS.OddLine.eq_zero_of_whiskerRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) {X Y : D} (f : X ⟶ Y) (h : CategoryTheory.MonoidalCategoryStruct.whiskerRight f L.obj = 0) : f = 0

A morphism killed by whiskering with the line vanishes.

Elementary cancellation helpers

theorem RS.eq_zero_of_iso_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] {W X Y Z : D} (a : W ≅ X) (f : X ⟶ Y) (b : Y ≅ Z) (h : CategoryTheory.CategoryStruct.comp a.hom (CategoryTheory.CategoryStruct.comp f b.hom) = 0) : f = 0

A morphism sandwiched between isomorphisms vanishes only if it vanishes.

theorem RS.smul_left_cancel_of_ne_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] {X Y : D} {a b : ℂ} {f : X ⟶ Y} (hf : f ≠ 0) (h : a • f = b • f) : a = b

Scalars are determined by their action on a nonzero morphism.

The unit of the free module

noncomputable def RS.algUnitHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] (W : D) : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W

The unit of the free module on an object, read in the ambient category.

Equations

• RS.algUnitHom R W = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one W)

theorem RS.algUnitHom_naturality {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {W W' : D} (k : W ⟶ W') : CategoryTheory.CategoryStruct.comp (algUnitHom R W) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R k) = CategoryTheory.CategoryStruct.comp k (algUnitHom R W')

The unit of the free module is natural.

theorem RS.algUnitHom_naturality_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {W W' : D} (k : W ⟶ W') {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj R W' ⟶ Z) : CategoryTheory.CategoryStruct.comp (algUnitHom R W) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R k) h) = CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp (algUnitHom R W') h)

The unit of the free module is natural.

theorem RS.algUnitHom_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] : CategoryTheory.CategoryStruct.comp (algUnitHom R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).hom = CategoryTheory.MonObj.one

At the tensor unit the free-module unit is the algebra unit.

def RS.UnitBij {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] (V W : D) : Prop

Postcomposition with the free-module unit is bijective.

Equations

• RS.UnitBij R V W = Function.Bijective fun (f : V ⟶ W) => CategoryTheory.CategoryStruct.comp f (RS.algUnitHom R W)

theorem RS.unitBij_biproduct_right {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (R : D) [CategoryTheory.MonObj R] {J : Type} [Finite J] (V : D) (g : J → D) (h : ∀ (k : J), UnitBij R V (g k)) : UnitBij R V (⨁ g)

The bijectivity statement passes to biproducts in the target.

theorem RS.unitBij_biproduct_left {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (R : D) [CategoryTheory.MonObj R] {J : Type} [Finite J] (f : J → D) (W : D) (h : ∀ (j : J), UnitBij R (f j) W) : UnitBij R (⨁ f) W

The bijectivity statement passes to biproducts in the source.

The atomic hom-sets

theorem RS.OddLine.hom_line_scalar {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (hsc : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), ∃ (c : ℂ), g = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (f : L.obj ⟶ L.obj) : ∃ (c : ℂ), f = c • CategoryTheory.CategoryStruct.id L.obj

Endomorphisms of the odd line are scalars when the endomorphisms of the tensor unit are.

theorem RS.OddLine.hom_unit_line_eq_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) (hLU : ∀ (g : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), g = 0) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ L.obj) : f = 0

Maps from the tensor unit to the odd line vanish when maps the other way do.

theorem RS.hom_unit_freeLine_eq_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) (R : D) (hLR : ∀ (f : L.obj ⟶ R), f = 0) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R L.obj) : g = 0

Maps from the tensor unit into the free module on the line vanish.

theorem RS.hom_line_freeUnit_eq_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (R : D) (hLR : ∀ (f : L.obj ⟶ R), f = 0) (g : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) : g = 0

Maps from the line into the free module on the tensor unit vanish.

theorem RS.algUnitHom_line {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (algUnitHom R L.obj) L.obj) (L.rot R).hom = CategoryTheory.CategoryStruct.comp L.sq.hom CategoryTheory.MonObj.one

The free-module unit at the line, transported through the rotation, is the algebra unit.

theorem RS.algUnitHom_unit_ne_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (R : D) [CategoryTheory.MonObj R] (hη : CategoryTheory.MonObj.one ≠ 0) : algUnitHom R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ≠ 0

The free-module unit at the tensor unit is nonzero.

theorem RS.algUnitHom_line_ne_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] (hη : CategoryTheory.MonObj.one ≠ 0) : algUnitHom R L.obj ≠ 0

The free-module unit at the line is nonzero.

theorem RS.hom_line_freeLine_scalar {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] (halg : ∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R), ∃ (c : ℂ), f = c • CategoryTheory.MonObj.one) (g : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R L.obj) : ∃ (c : ℂ), g = c • algUnitHom R L.obj

Maps from the line into the free module on the line are scalar multiples of the unit.

Bijectivity at the atoms

theorem RS.unitBij_unit_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] (R : D) [CategoryTheory.MonObj R] (hsc : ∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), ∃ (c : ℂ), f = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (halg : ∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R), ∃ (c : ℂ), f = c • CategoryTheory.MonObj.one) (hη : CategoryTheory.MonObj.one ≠ 0) : UnitBij R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)

The unit-to-unit case.

theorem RS.unitBij_unit_line {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] (hLU : ∀ (f : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), f = 0) (hLR : ∀ (f : L.obj ⟶ R), f = 0) : UnitBij R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.obj

The unit-to-line case.

theorem RS.unitBij_line_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] (hLU : ∀ (f : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), f = 0) (hLR : ∀ (f : L.obj ⟶ R), f = 0) : UnitBij R L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)

The line-to-unit case.

theorem RS.unitBij_line_line {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] (hsc : ∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), ∃ (c : ℂ), f = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (halg : ∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R), ∃ (c : ℂ), f = c • CategoryTheory.MonObj.one) (hη : CategoryTheory.MonObj.one ≠ 0) : UnitBij R L.obj L.obj

The line-to-line case.

Bijectivity at the mixed sums

theorem RS.unitBij_mix_right {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] (V : D) (h1 : UnitBij R V (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (h2 : UnitBij R V L.obj) (p q : ℕ) : UnitBij R V (L.mix p q)

Bijectivity at a mixed target follows from the two atoms.

theorem RS.unitBij_mix {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] (hsc : ∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), ∃ (c : ℂ), f = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (hLU : ∀ (f : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), f = 0) (halg : ∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R), ∃ (c : ℂ), f = c • CategoryTheory.MonObj.one) (hLR : ∀ (f : L.obj ⟶ R), f = 0) (hη : CategoryTheory.MonObj.one ≠ 0) (p q p' q' : ℕ) : UnitBij R (L.mix p q) (L.mix p' q')

Postcomposition with the free-module unit is bijective on mixed sums.

The free-module functor on mixed sums

theorem RS.freeModHomEquiv_freeModMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {V W : D} (f : V ⟶ W) : (freeModHomEquiv R V (freeMod R W)) (freeModMap R f) = CategoryTheory.CategoryStruct.comp f (algUnitHom R W)

Base change of a morphism corresponds, under the free–forgetful adjunction, to postcomposition with the free-module unit.

theorem RS.exists_preimage_freeModMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] (hsc : ∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), ∃ (c : ℂ), f = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (hLU : ∀ (f : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), f = 0) (halg : ∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R), ∃ (c : ℂ), f = c • CategoryTheory.MonObj.one) (hLR : ∀ (f : L.obj ⟶ R), f = 0) (hη : CategoryTheory.MonObj.one ≠ 0) (p q p' q' : ℕ) (g : freeMod R (L.mix p q) ⟶ freeMod R (L.mix p' q')) : ∃ (f : L.mix p q ⟶ L.mix p' q'), freeModMap R f = g

The free-module functor is full on mixed sums.

theorem RS.freeModMap_injective_mix {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] (hsc : ∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), ∃ (c : ℂ), f = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (hLU : ∀ (f : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), f = 0) (halg : ∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R), ∃ (c : ℂ), f = c • CategoryTheory.MonObj.one) (hLR : ∀ (f : L.obj ⟶ R), f = 0) (hη : CategoryTheory.MonObj.one ≠ 0) (p q p' q' : ℕ) : Function.Injective fun (f : L.mix p q ⟶ L.mix p' q') => freeModMap R f

The free-module functor is faithful on mixed sums.

theorem RS.id_unit_ne_zero_of_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (R : D) [CategoryTheory.MonObj R] (hη : CategoryTheory.MonObj.one ≠ 0) : CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ≠ 0

A nonzero algebra unit forces a nonzero identity on the tensor unit.

Idempotents of mixed sums split

theorem RS.OddLine.id_line_ne_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) (hid : CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ≠ 0) : CategoryTheory.CategoryStruct.id L.obj ≠ 0

The identity of the line is nonzero as soon as the identity of the tensor unit is.

noncomputable def RS.OddLine.mixEntry {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] (L : OddLine D) {p q p' q' : ℕ} (A : Matrix (Fin p) (Fin p') ℂ) (B : Matrix (Fin q) (Fin q') ℂ) (j : Fin p ⊕ Fin q) (k : Fin p' ⊕ Fin q') : L.mixFun p q j ⟶ L.mixFun p' q' k

The entries of a block-diagonal matrix on a mixed sum.

Equations

• L.mixEntry A B (Sum.inl i) (Sum.inl i') = A i i' • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)
• L.mixEntry A B (Sum.inl val) (Sum.inr val_1) = 0
• L.mixEntry A B (Sum.inr val) (Sum.inl val_1) = 0
• L.mixEntry A B (Sum.inr j) (Sum.inr j') = B j j' • CategoryTheory.CategoryStruct.id L.obj

noncomputable def RS.OddLine.mixMat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) {p q p' q' : ℕ} (A : Matrix (Fin p) (Fin p') ℂ) (B : Matrix (Fin q) (Fin q') ℂ) : ⨁ L.mixFun p q ⟶ ⨁ L.mixFun p' q'

A pair of complex matrices as a morphism of mixed sums.

Equations

• L.mixMat A B = CategoryTheory.Limits.biproduct.matrix (L.mixEntry A B)

theorem RS.OddLine.components_mixMat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) {p q p' q' : ℕ} (A : Matrix (Fin p) (Fin p') ℂ) (B : Matrix (Fin q) (Fin q') ℂ) (j : Fin p ⊕ Fin q) (k : Fin p' ⊕ Fin q') : CategoryTheory.Limits.biproduct.components (L.mixMat A B) j k = L.mixEntry A B j k

theorem RS.sum_smul_id {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] {X : D} {J : Type} [Fintype J] (u v : J → ℂ) : ∑ x : J, CategoryTheory.CategoryStruct.comp (u x • CategoryTheory.CategoryStruct.id X) (v x • CategoryTheory.CategoryStruct.id X) = (∑ x : J, u x * v x) • CategoryTheory.CategoryStruct.id X

Scalar multiples of an identity compose by multiplication.

theorem RS.OddLine.mixEntry_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] (L : OddLine D) {p q p' q' p'' q'' : ℕ} (A : Matrix (Fin p) (Fin p') ℂ) (B : Matrix (Fin q) (Fin q') ℂ) (A' : Matrix (Fin p') (Fin p'') ℂ) (B' : Matrix (Fin q') (Fin q'') ℂ) (j : Fin p ⊕ Fin q) (k : Fin p'' ⊕ Fin q'') : ∑ m : Fin p' ⊕ Fin q', CategoryTheory.CategoryStruct.comp (L.mixEntry A B j m) (L.mixEntry A' B' m k) = L.mixEntry (A * A') (B * B') j k

Block-diagonal matrices multiply blockwise.

theorem RS.OddLine.mixMat_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) {p q p' q' p'' q'' : ℕ} (A : Matrix (Fin p) (Fin p') ℂ) (B : Matrix (Fin q) (Fin q') ℂ) (A' : Matrix (Fin p') (Fin p'') ℂ) (B' : Matrix (Fin q') (Fin q'') ℂ) : CategoryTheory.CategoryStruct.comp (L.mixMat A B) (L.mixMat A' B') = L.mixMat (A * A') (B * B')

Composition of block matrices is matrix multiplication.

theorem RS.OddLine.mixMat_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) : L.mixMat 1 1 = CategoryTheory.CategoryStruct.id (⨁ L.mixFun p q)

The identity matrices give the identity morphism.

theorem RS.OddLine.exists_mixMat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (hsc : ∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), ∃ (c : ℂ), f = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (hLU : ∀ (f : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), f = 0) {p q : ℕ} (e : ⨁ L.mixFun p q ⟶ ⨁ L.mixFun p q) : ∃ (A : Matrix (Fin p) (Fin p) ℂ) (B : Matrix (Fin q) (Fin q) ℂ), e = L.mixMat A B

Every endomorphism of a mixed sum is a pair of complex matrices.

theorem RS.OddLine.mixMat_injective {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (hid : CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ≠ 0) {p q p' q' : ℕ} {A A' : Matrix (Fin p) (Fin p') ℂ} {B B' : Matrix (Fin q) (Fin q') ℂ} (h : L.mixMat A B = L.mixMat A' B') : A = A' ∧ B = B'

The pair of matrices is determined by the morphism.

theorem RS.exists_split_of_idem_mix {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (hsc : ∀ (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), ∃ (c : ℂ), f = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (hLU : ∀ (f : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D), f = 0) (hid : CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ≠ 0) {p q : ℕ} (e : L.mix p q ⟶ L.mix p q) (he : CategoryTheory.CategoryStruct.comp e e = e) : ∃ (p' : ℕ) (q' : ℕ) (a : L.mix p' q' ⟶ L.mix p q) (b : L.mix p q ⟶ L.mix p' q'), CategoryTheory.CategoryStruct.comp a b = CategoryTheory.CategoryStruct.id (L.mix p' q') ∧ CategoryTheory.CategoryStruct.comp b a = e

An idempotent endomorphism of a mixed sum splits off a mixed sum.