copy — Mathlib

English

Copying a coalgebra morphism with the new function equal to the old one yields the same morphism

Русский

Копирование коалгоморфизма с новой функцией, равной старой, даёт тот же морфизм

LaTeX

$$$$ f.copy f' h = f $$$$

Lean4

/-- Copy of a `CoalgHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : A →ₗc[R] B) (f' : A → B) (h : f' = ⇑f) : A →ₗc[R] B :=
  { toLinearMap := (f : A →ₗ[R] B).copy f' h
    counit_comp := by ext; simp_all
    map_comp_comul := by simp only [(f : A →ₗ[R] B).copy_eq f' h, CoalgHomClass.map_comp_comul] }

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