unop — Mathlib

English

The unopposite of a non-unital ring hom Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ is inverse to op.

Русский

Обратное отображение (unop) неабсолютного гомоморфизма Rᵐᵒᵖ → Sᵐᵒᵖ является обратным к op.

LaTeX

$$$\text{NonUnitalRingHom}^{-1} = \text{unop}$, i.e.\: \operatorname{NonUnitalRingHom}(R^{\mathrm{op}}, S^{\mathrm{op}}) \cong \operatorname{NonUnitalRingHom}(R,S)$$$

Lean4

/-- The 'unopposite' of a non-unital ring hom `Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ`. Inverse to
`NonUnitalRingHom.op`. -/
@[simp]
def unop {R S} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ) ≃ (R →ₙ+* S) :=
  NonUnitalRingHom.op.symm

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