ℂ-linearity from the scalar unit

A preadditive monoidal category whose unit endomorphisms are identified with ℂ carries a ℂ-linear structure on every hom-set: the scalar c acts by conjugating the unit endomorphism φ c through the left unitor and composing. The file proves the module laws and assembles CategoryTheory.Linear ℂ D from a single ring isomorphism φ : ℂ ≃+* End (𝟙_ D), then instantiates the input at Ind C: the unit of the transported monoidal structure is the embedded unit (RS.indOfUnitIso), so a scalar unit for C induces one for Ind C (RS.indScalarUnit).

Two points of care.

• End-multiplication is reversed composition, and ℂ is commutative; RS.scalarUnit_map_mul records the translation φ (a * b) = φ a ≫ φ b on which mul_smul rests.
• The monoidal-linear laws need more than the module laws: left whiskering moves the scalar to the right leg of the tensor, so whiskerLeft_smul needs the left-unitor conjugate of φ c ▷ X to agree with the right-unitor conjugate of X ◁ φ c. This is not a theorem of general monoidal categories (in bimodules over a commutative ring R with an automorphism, the two conjugates differ on twisted bimodules even when End (𝟙) = ℂ), but it holds in braided ones. The agreement is therefore isolated as the hypothesis RS.ScalarBalanced, discharged for braided categories by RS.scalarBalanced_of_braided.

Everything here is a def or a theorem, never an instance: a global Linear ℂ instance built from an arbitrary φ would clash with existing linear structures (and with itself, for two different φ), so callers install the structure with letI at use sites.

The scalar action of the unit's endomorphisms

def RS.scalarHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (c : ℂ) : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D

The unit endomorphism φ c, typed as a morphism rather than as an element of the endomorphism ring, so that sums and composites of these values elaborate at the hom-set instances.

Equations

• RS.scalarHom φ c = φ c

theorem RS.scalarUnit_map_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (a b : ℂ) : scalarHom φ (a * b) = CategoryTheory.CategoryStruct.comp (scalarHom φ a) (scalarHom φ b)

End-multiplication is reversed composition, and ℂ is commutative, so a ring isomorphism out of ℂ turns products into composites in either order; this is the composition-order reading used throughout.

def RS.scalarEnd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (c : ℂ) (X : D) : X ⟶ X

The scalar c as an endomorphism of X: whisker the unit endomorphism φ c onto X and cancel the unit through the left unitor.

Equations

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

theorem RS.scalarEnd_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (X : D) : scalarEnd φ 1 X = CategoryTheory.CategoryStruct.id X

The scalar 1 acts as the identity.

theorem RS.scalarEnd_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (a b : ℂ) (X : D) : scalarEnd φ (a * b) X = CategoryTheory.CategoryStruct.comp (scalarEnd φ a X) (scalarEnd φ b X)

The action turns multiplication into composition.

theorem RS.scalarEnd_naturality {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (c : ℂ) {X Y : D} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (scalarEnd φ c X) f = CategoryTheory.CategoryStruct.comp f (scalarEnd φ c Y)

The scalar action is central: it exchanges with every morphism. Left-unitor naturality moves the unitors across f, and the whisker exchange moves φ c ▷ − across 𝟙 ◁ f.

theorem RS.scalarEnd_whiskerRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (c : ℂ) (X Y : D) : CategoryTheory.MonoidalCategoryStruct.whiskerRight (scalarEnd φ c X) Y = scalarEnd φ c (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The scalar action whiskers on the right: the left-unitor conjugate at X ⊗ Y restricts to the one at X.

def RS.ScalarBalanced {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) : Prop

The two-sided agreement of the unit action: the left-unitor conjugate of φ c ▷ X is the right-unitor conjugate of X ◁ φ c. This is not automatic in a monoidal category — bimodule categories with End (𝟙) = ℂ can act by different ring embeddings on the two sides of an object — and it is exactly what the monoidal-linear law for left whiskering needs, so it is a named hypothesis, discharged in the braided case by RS.scalarBalanced_of_braided.

Equations

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

theorem RS.scalarBalanced_of_braided {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.BraidedCategory D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) : ScalarBalanced φ

In a braided category the unit action is balanced: the braiding with the unit carries φ c ▷ X to X ◁ φ c and exchanges the two unitors.

theorem RS.whiskerLeft_unitConj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (X Y : D) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight u Y) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom)) = CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X u) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)) Y

Left whiskering carries the left-unitor conjugate of a unit endomorphism into the right-unitor conjugate, whiskered on the right: the triangle identity trades X ◁ (λ_ Y) for (ρ_ X) ▷ Y around the middle associator.

theorem RS.whiskerLeft_scalarEnd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (h : ScalarBalanced φ) (c : ℂ) (X Y : D) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (scalarEnd φ c Y) = scalarEnd φ c (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The scalar action whiskers on the left, given the two-sided agreement, which converts the right-unitor data produced by RS.whiskerLeft_unitConj back to left-unitor data at X.

The hom-set modules and the linear structure

theorem RS.scalarEnd_add {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (a b : ℂ) (X : D) : scalarEnd φ (a + b) X = scalarEnd φ a X + scalarEnd φ b X

The action is additive in the scalar.

theorem RS.scalarEnd_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (X : D) : scalarEnd φ 0 X = 0

The scalar 0 acts as zero.

def RS.scalarSmul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) {X Y : D} (c : ℂ) (f : X ⟶ Y) : X ⟶ Y

The scalar action on a hom-set: whisker the unit endomorphism through the left unitor of the source and compose.

Equations

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

theorem RS.scalarSmul_eq {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) {X Y : D} (c : ℂ) (f : X ⟶ Y) : scalarSmul φ c f = CategoryTheory.CategoryStruct.comp (scalarEnd φ c X) f

The action on morphisms is composition with the endomorphism form of the scalar.

@[reducible]

def RS.scalarModule {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (X Y : D) : Module ℂ (X ⟶ Y)

The ℂ-module structure on a hom-set induced by the scalar unit.

Equations

• RS.scalarModule φ X Y = { smul := fun (c : ℂ) (f : X ⟶ Y) => RS.scalarSmul φ c f, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[reducible]

def RS.linearOfScalarUnit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) : CategoryTheory.Linear ℂ D

ℂ-linearity from the scalar unit: a ring isomorphism ℂ ≃+* End (𝟙_ D) makes a preadditive monoidal category ℂ-linear. A def, not an instance: an unconditional instance would clash with every existing linear structure, so callers install it by letI.

Equations

• RS.linearOfScalarUnit φ = { homModule := fun (X Y : D) => RS.scalarModule φ X Y, smul_comp := ⋯, comp_smul := ⋯ }

theorem RS.monoidalLinearOfScalarUnit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (h : ScalarBalanced φ) : CategoryTheory.MonoidalLinear ℂ D

Monoidal ℂ-linearity from the scalar unit, given the two-sided agreement of the unit action: whiskering is ℂ-linear in each variable. Stated under letI := linearOfScalarUnit φ; use it the same way.

theorem RS.monoidalLinearOfScalarUnitBraided {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.BraidedCategory D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) : CategoryTheory.MonoidalLinear ℂ D

Monoidal ℂ-linearity from the scalar unit in a braided category, where the two-sided agreement is automatic.

Endomorphism rings under isomorphism and embedding

def RS.endCongrRingEquiv {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] {X Y : E} (α : X ≅ Y) : CategoryTheory.End X ≃+* CategoryTheory.End Y

Conjugation by an isomorphism as a ring equivalence of endomorphism rings; conjugation preserves the reversed products because the connecting isomorphisms cancel in the middle.

Equations

• RS.endCongrRingEquiv α = { toEquiv := α.conj.toEquiv, map_mul' := ⋯, map_add' := ⋯ }

The scalar unit of Ind C

theorem RS.indOf_additive {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] : indOf.Additive

The embedding C ⥤ Ind C is additive: it preserves finite colimits, hence binary biproducts, between preadditive categories.

noncomputable def RS.indOfEndRingEquiv {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] (x : C) : CategoryTheory.End x ≃+* CategoryTheory.End (indOf.obj x)

Full faithfulness of the embedding on endomorphisms, as a ring equivalence; End-multiplication is reversed composition on both sides, so functoriality preserves it verbatim.

Equations

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

noncomputable def RS.indScalarUnit {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] (ψ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C))

The scalar unit of Ind C: a ring isomorphism ℂ ≃+* End (𝟙_ C) transports along the embedding and the unit identification to one for Ind C.

Equations

• RS.indScalarUnit ψ = (ψ.trans (RS.indOfEndRingEquiv (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).trans (RS.endCongrRingEquiv RS.indOfUnitIso.symm)

Acceptance