comp_apply — Mathlib

English

Applying a morphism to a pseudoelement is compatible with composition: applying f and then g is the same as applying their composition to the pseudoelement.

Русский

Применение морфизма к псевдоэлементу совместимо с композицией: применение f затем g эквивалентно применению их композиции к псевдоэлементу.

LaTeX

$$$\\mathrm{pseudoApply}(g)\\bigl(\\mathrm{pseudoApply}(f)(a)\\bigr) = \\mathrm{pseudoApply}(f\\circ g)(a)$$$

Lean4

/-- Applying a pseudoelement to a composition of morphisms is the same as composing
with each morphism. Sadly, this is not a definitional equality, but at least it is true. -/
theorem comp_apply {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) (a : P) : (f ≫ g) a = g (f a) :=
  Quotient.inductionOn a fun x =>
    Quotient.sound <| by
      simp only [app]
      rw [← Category.assoc, Over.coe_hom]

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