CategoryTheory.Linear.units_smul_comp
theorem CategoryTheory.Linear.units_smul_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type w}
[inst_2 : Semiring R] [inst_3 : CategoryTheory.Linear R C] {X Y Z : C} (r : Rˣ) (f : X ⟶ Y) (g : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp (r • f) g = r • CategoryTheory.CategoryStruct.comp f g
The theorem `CategoryTheory.Linear.units_smul_comp` states that for any category `C` which is also preadditive, any semiring `R`, and any linear map between `R` and `C`, along with objects `X, Y, Z` of the category `C`, any unit `r` of `R` and morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, the composition of the scaled morphism `r • f` with `g` is the same as the morphism obtained by scaling the composition of `f` and `g` by `r`. In mathematical terms, it asserts that `(r • f) ∘ g = r • (f ∘ g)`.
More concisely: For any preadditive category `C`, semiring `R`, linear map `f: R ⊓ C -> C`, objects `X, Y, Z` of `C`, unit `r` of `R`, and morphisms `f: X -> Y` and `g: Y -> Z` in `C`, `(r • f) ∘ g = r • (f ∘ g)`.
|
CategoryTheory.Linear.comp_units_smul
theorem CategoryTheory.Linear.comp_units_smul :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type w}
[inst_2 : Semiring R] [inst_3 : CategoryTheory.Linear R C] {X Y Z : C} (f : X ⟶ Y) (r : Rˣ) (g : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g
This theorem, named `CategoryTheory.Linear.comp_units_smul`, states that for any categories `C`, with additional structures of preadditivity and being linear over a semiring `R`, and for any three objects `X`, `Y`, and `Z` in `C`, the composition of a morphism `f` from `X` to `Y` and a scalar multiple `r • g` of another morphism `g` from `Y` to `Z` is the same as the scalar multiple `r •` of the composition of `f` and `g`.
In other words, it states that scalar multiplication interacts with composition of morphisms in the same way as it does in linear algebra: `(f ∘ (r · g)) = r · (f ∘ g)`, where '∘' denotes composition of morphisms, '·' denotes scalar multiplication, and `r` is an element from the semiring `R`.
More concisely: For any morphisms $f : X \to Y$ and $g : Y \to Z$ in a preadditive, linear category over a semiring $R$, the composition $f \circ (r \cdot g) = r \cdot (f \circ g)$, where $r \in R$ and $\cdot$ denotes scalar multiplication and composition respectively.
|
CategoryTheory.Linear.smul_comp
theorem CategoryTheory.Linear.smul_comp :
∀ {R : Type w} [inst : Semiring R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
[inst_2 : CategoryTheory.Preadditive C] [self : CategoryTheory.Linear R C] (X Y Z : C) (r : R) (f : X ⟶ Y)
(g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (r • f) g = r • CategoryTheory.CategoryStruct.comp f g
The theorem `CategoryTheory.Linear.smul_comp` states that for any semiring `R`, any category `C` that is also preadditive, any `CategoryTheory.Linear` structure on `R` and `C`, any three objects `X`, `Y`, `Z` in `C`, any scalar `r` from `R`, and any two morphisms `f` from `X` to `Y` and `g` from `Y` to `Z` in `C`, the composition of the scalar multiplication of `r` and `f`, followed by `g`, is equal to the scalar multiplication of `r` and the composition of `f` followed by `g`. In mathematical terms, this is stating $(r \cdot f) \circ g = r \cdot (f \circ g)$, where $\circ$ denotes composition of morphisms, and $\cdot$ denotes scalar multiplication.
More concisely: For any semiring R, preadditive category C with a Linear structure, and morphisms f : X -> Y and g : Y -> Z in C, the scalar multiplication of r in R and the composition of f and g is equal to the composition of the scalar multiplication of r and f, followed by g. In other words, r * (f * g) = (r * f) * g.
|
CategoryTheory.Linear.comp_smul
theorem CategoryTheory.Linear.comp_smul :
∀ {R : Type w} [inst : Semiring R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
[inst_2 : CategoryTheory.Preadditive C] [self : CategoryTheory.Linear R C] (X Y Z : C) (f : X ⟶ Y) (r : R)
(g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g
The theorem `CategoryTheory.Linear.comp_smul` states that for any semiring `R`, any category `C` that is preadditive, and any linear structure of `R` on `C`, the process of scalar multiplication, denoted by `r • g`, is compatible with pre-composition in the category. More specifically, for any three objects `X`, `Y`, and `Z` in the category `C`, and any morphisms `f` from `X` to `Y`, and `g` from `Y` to `Z`, pre-composing `f` with the result of scaling `g` by `r` (i.e., `r • g`) is the same as scaling the pre-composition of `f` and `g` by `r`. This is expressed in Lean as `CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g`.
This is a property that is expected in a category that has additional linear structure.
More concisely: For any semiring `R`, preadditive category `C` with a linear structure, and morphisms `f : X → Y` and `g : Y → Z` in `C`, the scalar multiplication `r • g` commutes with composition, i.e., `CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g`.
|