English
Let R be a commutative semiring and A an R-algebra. Consider the linear equivalence between A and its opposite A^op. Then the preimage of the unit submodule under this isomorphism is the unit submodule itself.
Русский
Пусть R—коммутативное полугрупповое кольцо и A — R-алгебра. Рассматривая линейное эквивалентство между A и его противоположностью A^op, предобраз единичного подмодуля по этому изоморфизму равен единичному подмодулю.
LaTeX
$$$\\phi^{-1}(A)=A$, where $\\phi$ is the linear isomorphism $A \\to A^{op}$ corresponding to the opposite.$$
Lean4
@[simp]
theorem comap_unop_one : comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (1 : Submodule R A) = 1 := by
rw [← map_equiv_eq_comap_symm, map_op_one]
