Documentation

Mathlib.Algebra.Ring.Subsemiring.MulOpposite

Subsemiring of opposite semirings #

For every semiring R, we construct an equivalence between subsemirings of R and that of Rᵐᵒᵖ.

@[simp]
theorem Subsemiring.op_toSubmonoid {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
S.op.toSubmonoid = S.op

Pull a subsemiring back to an opposite subsemiring along MulOpposite.unop

Equations
  • S.op = { toSubmonoid := S.op, add_mem' := , zero_mem' := }
Instances For
    @[simp]
    theorem Subsemiring.op_coe {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
    S.op = MulOpposite.unop ⁻¹' S
    @[simp]
    theorem Subsemiring.mem_op {R : Type u_2} [NonAssocSemiring R] {x : Rᵐᵒᵖ} {S : Subsemiring R} :
    @[simp]
    theorem Subsemiring.unop_toSubmonoid {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring Rᵐᵒᵖ) :
    S.unop.toSubmonoid = S.unop

    Pull an opposite subsemiring back to a subsemiring along MulOpposite.op

    Equations
    • S.unop = { toSubmonoid := S.unop, add_mem' := , zero_mem' := }
    Instances For
      @[simp]
      theorem Subsemiring.unop_coe {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring Rᵐᵒᵖ) :
      S.unop = MulOpposite.op ⁻¹' S
      @[simp]
      theorem Subsemiring.mem_unop {R : Type u_2} [NonAssocSemiring R] {x : R} {S : Subsemiring Rᵐᵒᵖ} :
      x S.unop MulOpposite.op x S
      @[simp]
      theorem Subsemiring.unop_op {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
      S.op.unop = S
      @[simp]
      theorem Subsemiring.op_unop {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring Rᵐᵒᵖ) :
      S.unop.op = S

      Lattice results #

      theorem Subsemiring.op_le_iff {R : Type u_2} [NonAssocSemiring R] {S₁ : Subsemiring R} {S₂ : Subsemiring Rᵐᵒᵖ} :
      S₁.op S₂ S₁ S₂.unop
      theorem Subsemiring.le_op_iff {R : Type u_2} [NonAssocSemiring R] {S₁ : Subsemiring Rᵐᵒᵖ} {S₂ : Subsemiring R} :
      S₁ S₂.op S₁.unop S₂
      @[simp]
      theorem Subsemiring.op_le_op_iff {R : Type u_2} [NonAssocSemiring R] {S₁ : Subsemiring R} {S₂ : Subsemiring R} :
      S₁.op S₂.op S₁ S₂
      @[simp]
      theorem Subsemiring.unop_le_unop_iff {R : Type u_2} [NonAssocSemiring R] {S₁ : Subsemiring Rᵐᵒᵖ} {S₂ : Subsemiring Rᵐᵒᵖ} :
      S₁.unop S₂.unop S₁ S₂
      @[simp]
      theorem Subsemiring.opEquiv_symm_apply {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring Rᵐᵒᵖ) :
      (RelIso.symm Subsemiring.opEquiv) S = S.unop
      @[simp]
      theorem Subsemiring.opEquiv_apply {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
      Subsemiring.opEquiv S = S.op

      A subsemiring S of R determines a subsemiring S.op of the opposite ring Rᵐᵒᵖ.

      Equations
      • Subsemiring.opEquiv = { toFun := Subsemiring.op, invFun := Subsemiring.unop, left_inv := , right_inv := , map_rel_iff' := }
      Instances For
        @[simp]
        theorem Subsemiring.op_inj {R : Type u_2} [NonAssocSemiring R] {S : Subsemiring R} {T : Subsemiring R} :
        S.op = T.op S = T
        @[simp]
        theorem Subsemiring.unop_inj {R : Type u_2} [NonAssocSemiring R] {S : Subsemiring Rᵐᵒᵖ} {T : Subsemiring Rᵐᵒᵖ} :
        S.unop = T.unop S = T
        @[simp]
        theorem Subsemiring.op_bot {R : Type u_2} [NonAssocSemiring R] :
        .op =
        @[simp]
        theorem Subsemiring.op_eq_bot {R : Type u_2} [NonAssocSemiring R] {S : Subsemiring R} :
        S.op = S =
        @[simp]
        theorem Subsemiring.unop_bot {R : Type u_2} [NonAssocSemiring R] :
        .unop =
        @[simp]
        @[simp]
        theorem Subsemiring.op_top {R : Type u_2} [NonAssocSemiring R] :
        .op =
        @[simp]
        theorem Subsemiring.op_eq_top {R : Type u_2} [NonAssocSemiring R] {S : Subsemiring R} :
        S.op = S =
        @[simp]
        theorem Subsemiring.unop_top {R : Type u_2} [NonAssocSemiring R] :
        .unop =
        @[simp]
        theorem Subsemiring.op_sup {R : Type u_2} [NonAssocSemiring R] (S₁ : Subsemiring R) (S₂ : Subsemiring R) :
        (S₁ S₂).op = S₁.op S₂.op
        theorem Subsemiring.unop_sup {R : Type u_2} [NonAssocSemiring R] (S₁ : Subsemiring Rᵐᵒᵖ) (S₂ : Subsemiring Rᵐᵒᵖ) :
        (S₁ S₂).unop = S₁.unop S₂.unop
        theorem Subsemiring.op_inf {R : Type u_2} [NonAssocSemiring R] (S₁ : Subsemiring R) (S₂ : Subsemiring R) :
        (S₁ S₂).op = S₁.op S₂.op
        theorem Subsemiring.unop_inf {R : Type u_2} [NonAssocSemiring R] (S₁ : Subsemiring Rᵐᵒᵖ) (S₂ : Subsemiring Rᵐᵒᵖ) :
        (S₁ S₂).unop = S₁.unop S₂.unop
        theorem Subsemiring.op_sSup {R : Type u_2} [NonAssocSemiring R] (S : Set (Subsemiring R)) :
        (sSup S).op = sSup (Subsemiring.unop ⁻¹' S)
        theorem Subsemiring.unop_sSup {R : Type u_2} [NonAssocSemiring R] (S : Set (Subsemiring Rᵐᵒᵖ)) :
        (sSup S).unop = sSup (Subsemiring.op ⁻¹' S)
        theorem Subsemiring.op_sInf {R : Type u_2} [NonAssocSemiring R] (S : Set (Subsemiring R)) :
        (sInf S).op = sInf (Subsemiring.unop ⁻¹' S)
        theorem Subsemiring.unop_sInf {R : Type u_2} [NonAssocSemiring R] (S : Set (Subsemiring Rᵐᵒᵖ)) :
        (sInf S).unop = sInf (Subsemiring.op ⁻¹' S)
        theorem Subsemiring.op_iSup {ι : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ιSubsemiring R) :
        (iSup S).op = ⨆ (i : ι), (S i).op
        theorem Subsemiring.unop_iSup {ι : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ιSubsemiring Rᵐᵒᵖ) :
        (iSup S).unop = ⨆ (i : ι), (S i).unop
        theorem Subsemiring.op_iInf {ι : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ιSubsemiring R) :
        (iInf S).op = ⨅ (i : ι), (S i).op
        theorem Subsemiring.unop_iInf {ι : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ιSubsemiring Rᵐᵒᵖ) :
        (iInf S).unop = ⨅ (i : ι), (S i).unop
        theorem Subsemiring.op_closure {R : Type u_2} [NonAssocSemiring R] (s : Set R) :
        (Subsemiring.closure s).op = Subsemiring.closure (MulOpposite.unop ⁻¹' s)
        @[simp]
        theorem Subsemiring.addEquivOp_apply_coe {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) (a : S.toSubmonoid) :
        (S.addEquivOp a) = MulOpposite.op a
        @[simp]
        theorem Subsemiring.addEquivOp_symm_apply_coe {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) (b : S.op) :
        (S.addEquivOp.symm b) = MulOpposite.unop b
        def Subsemiring.addEquivOp {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
        S ≃+ S.op

        Bijection between a subsemiring S and its opposite.

        Equations
        • S.addEquivOp = { toEquiv := S.equivOp, map_add' := }
        Instances For
          @[simp]
          theorem Subsemiring.ringEquivOpMop_symm_apply_coe {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
          ∀ (a : (↥S.op)ᵐᵒᵖ), (S.ringEquivOpMop.symm a) = MulOpposite.unop (MulOpposite.unop a)
          @[simp]
          theorem Subsemiring.ringEquivOpMop_apply {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
          ∀ (a : S), S.ringEquivOpMop a = MulOpposite.op (S.addEquivOp a)

          Bijection between a subsemiring S and MulOpposite of its opposite.

          Equations
          • S.ringEquivOpMop = { toEquiv := (S.addEquivOp.trans MulOpposite.opAddEquiv).toEquiv, map_mul' := , map_add' := }
          Instances For
            @[simp]
            theorem Subsemiring.mopRingEquivOp_apply_coe {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
            ∀ (a : (↥S)ᵐᵒᵖ), (S.mopRingEquivOp a) = MulOpposite.op (MulOpposite.unop a)
            @[simp]
            theorem Subsemiring.mopRingEquivOp_symm_apply {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
            ∀ (a : S.op), S.mopRingEquivOp.symm a = MulOpposite.op (S.addEquivOp.symm a)

            Bijection between MulOpposite of a subsemiring S and its opposite.

            Equations
            • S.mopRingEquivOp = { toEquiv := (MulOpposite.opAddEquiv.symm.trans S.addEquivOp).toEquiv, map_mul' := , map_add' := }
            Instances For