copy — Mathlib

English

Copying a morphism with a new function component yields an equal morphism if the new function matches the old one.

Русский

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

LaTeX

$$$f.copy\\, f'\\, h = f$$$

Lean4

/-- Copy of a `BialgHom` 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 :=
  { toCoalgHom := (f : A →ₗc[R] B).copy f' h
    map_one' := by simp_all
    map_mul' := by intros; simp_all }

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