asIdealOpposite — Mathlib

English

There is a notion of taking the opposite ring; the two-sided ideal I corresponds to a right-ideal in the opposite ring via asIdealOpposite, with elements related by op/unop.

Русский

Существует представление двустороннего идеала через противоположное кольцо с помощью asIdealOpposite, где элементы связаны через операции op/unop.

LaTeX

$$$I\mapsto I.asIdealOpposite : TwoSidedIdeal R \to Ideal\; R^{op}$$$

Lean4

/-- Every two-sided ideal is also a right ideal. -/
def asIdealOpposite : TwoSidedIdeal R →o Ideal Rᵐᵒᵖ
    where
  toFun I := asIdeal ⟨I.ringCon.op⟩
  monotone' I J h x
    h' := by
    simp only [mem_asIdeal, mem_iff, RingCon.op_iff, MulOpposite.unop_zero] at h' ⊢
    exact J.rel_iff _ _ |>.2 <| h <| I.rel_iff 0 x.unop |>.1 h'

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