English
For algebra isomorphisms e and e' and e2,e2' mapping A1→A2 to A1'→A2' and A2→A3 to A2'→A3', transportations respect composition: arrowCongr (e.trans e2) (e1'.trans e2') = (arrowCongr e e1').trans (arrowCongr e2 e2').
Русский
Для изоморфизмов \(e,e'\) и соответствующих отображений между последовательностями сохраняется композиция при переносе.
LaTeX
$$$\\text{arrowCongr }(e_1,e_2)\\text{ is compatible with composition: }\\arrowCongr (e_1\\!\\trans e_2) (e_1'\\!\\trans e_2') = (\\arrowCongr e_1 e_1').trans (\\arrowCongr e_2 e_2').$$$
Lean4
/-- If `A₁` is equivalent to `A₂` and `A₁'` is equivalent to `A₂'`, then the type of maps
`A₁ ≃ₐ[R] A₁'` is equivalent to the type of maps `A₂ ≃ₐ[R] A₂'`.
This is the `AlgEquiv` version of `AlgEquiv.arrowCongr`. -/
@[simps apply]
def equivCongr (e : A₁ ≃ₐ[R] A₂) (e' : A₁' ≃ₐ[R] A₂') : (A₁ ≃ₐ[R] A₁') ≃ A₂ ≃ₐ[R] A₂'
where
toFun ψ := e.symm.trans (ψ.trans e')
invFun ψ := e.trans (ψ.trans e'.symm)
left_inv
ψ := by
ext
simp_rw [trans_apply, symm_apply_apply]
right_inv
ψ := by
ext
simp_rw [trans_apply, apply_symm_apply]
