English
There is a canonical equivalence between maps A1 →ₐ[R] A2 and A1' →ₐ[R] A2' obtained by transporting via given equivalences, with explicit forward and inverse mappings.
Русский
Существует каноническое эквивалентное отображение между гомоморфизмами через заданные эквивалентности.
LaTeX
$$$\text{arrowCongr}(e_1,e_2): (A_1 \toₐ[R] A_2) \simeq (A_1' \toₐ[R] A_2')$$$
Lean4
/-- `Equiv.cast (congrArg _ h)` as an algebra equiv.
Note that unlike `Equiv.cast`, this takes an equality of indices rather than an equality of types,
to avoid having to deal with an equality of the algebraic structure itself. -/
@[simps!]
protected def cast {ι : Type*} {A : ι → Type*} [∀ i, Semiring (A i)] [∀ i, Algebra R (A i)] {i j : ι} (h : i = j) :
A i ≃ₐ[R] A j where
__ := RingEquiv.cast h
commutes' _ := by cases h; rfl
