hom_comp — Mathlib

English

Composition in FGModuleCat corresponds to composition of underlying linear maps: (f ≫ g).hom = g.hom ∘ f.hom.

Русский

Сложение морфизмов в FGModuleCat эквивалентно композиции линейных отображений: (f ≫ g).hom = g.hom ∘ f.hom.

LaTeX

$$$ (f \\gg g).\\mathrm{hom} = g.\\mathrm{hom} \\circ f.\\mathrm{hom} $$$

Lean4

@[simp]
theorem hom_comp (A B C : FGModuleCat.{v} R) (f : A ⟶ B) (g : B ⟶ C) : (f ≫ g).hom = g.hom.comp f.hom :=
  rfl

Похожие утверждения