English
The linear map underlying the opposite-constructed algebra hom equals the composition with the opposite-linear-equivalence.
Русский
Линейное отображение, лежащее в основе противоположного отображения, равняется композиции с противоположной линейной эквалентностью.
LaTeX
$$(f.toOpposite hf).toLinearMap = (opLinearEquiv R) ∘ f.toLinearMap$$
Lean4
/-- An algebra homomorphism `f : A →ₐ[R] B` such that `f x` commutes with `f y` for all `x, y` defines
an algebra homomorphism from `Aᵐᵒᵖ`. -/
@[simps -fullyApplied]
def fromOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) : Aᵐᵒᵖ →ₐ[R] B :=
{ f.toRingHom.fromOpposite hf with
toFun := f ∘ unop
commutes' := fun r => f.commutes r }
