comp — Mathlib

English

The coercion of the composition equals the composition of the coercions

Русский

Коэрция композиции равна композиции коэрций

LaTeX

$$$$ \uparrow (\phi_1.comp \phi_2) = (\uparrow \phi_1) \circ (\uparrow \phi_2) $$$$

Lean4

/-- Composition of coalgebra homomorphisms. -/
@[simps!]
def comp (φ₁ : B →ₗc[R] C) (φ₂ : A →ₗc[R] B) : A →ₗc[R] C :=
  { (φ₁ : B →ₗ[R] C) ∘ₗ (φ₂ : A →ₗ[R] B) with
    counit_comp := by ext; simp
    map_comp_comul := by ext; simp [map_comp] }

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