English
Copying a ContinuousAlgHom with a new function f' equal to the old one yields an equal ContinuousAlgHom with the new function.
Русский
Копирование ContinuousAlgHom с новой функцией f' эквивалентно созданию равного ContinuousAlgHom с новой функцией.
LaTeX
$$$\\text{copy}~(f:A \\toA[R] B)~(f':A \\to B)~(h:f' = \\!\\!f) : A \\toA[R] B$$$
Lean4
/-- Copy of a `ContinuousAlgHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
def copy (f : A →A[R] B) (f' : A → B) (h : f' = ⇑f) : A →A[R] B
where
toAlgHom :=
{ toRingHom := (f : A →A[R] B).toRingHom.copy f' h
commutes' := fun r => by
simp only [AlgHom.toRingHom_eq_coe, h, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
MonoidHom.coe_coe, RingHom.coe_copy, AlgHomClass.commutes f r] }
cont := show Continuous f' from h.symm ▸ f.continuous
