Documentation

Mathlib.RingTheory.TwoSidedIdeal.Basic

Two Sided Ideals #

In this file, for any Ring R, we reinterpret I : RingCon R as a two-sided-ideal of a ring.

Main definitions and results #

structure TwoSidedIdeal (R : Type u_1) [NonUnitalNonAssocRing R] :
Type u_1

A two-sided ideal of a ring R is a subset of R that contains 0 and is closed under addition, negation, and absorbs multiplication on both sides.

  • ringCon : RingCon R

    every two-sided-ideal is induced by a congruence relation on the ring.

Instances For
    Equations
    • TwoSidedIdeal.setLike = { coe := fun (t : TwoSidedIdeal R) => {r : R | t.ringCon r 0}, coe_injective' := }
    theorem TwoSidedIdeal.mem_iff {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (x : R) :
    x I I.ringCon x 0
    theorem TwoSidedIdeal.rel_iff {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (x : R) (y : R) :
    I.ringCon x y x - y I
    @[simp]
    theorem TwoSidedIdeal.coeOrderEmbedding_apply {R : Type u_1} [NonUnitalNonAssocRing R] :
    ∀ (a : TwoSidedIdeal R), TwoSidedIdeal.coeOrderEmbedding a = a

    the coercion from two-sided-ideals to sets is an order embedding

    Equations
    • TwoSidedIdeal.coeOrderEmbedding = { toFun := SetLike.coe, inj' := , map_rel_iff' := }
    Instances For
      theorem TwoSidedIdeal.le_iff {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} {J : TwoSidedIdeal R} :
      I J I J

      Two-sided-ideals corresponds to congruence relations on a ring.

      Equations
      • TwoSidedIdeal.orderIsoRingCon = { toFun := TwoSidedIdeal.ringCon, invFun := TwoSidedIdeal.mk, left_inv := , right_inv := , map_rel_iff' := }
      Instances For
        theorem TwoSidedIdeal.ringCon_le_iff {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} {J : TwoSidedIdeal R} :
        I J I.ringCon J.ringCon
        theorem TwoSidedIdeal.ext_iff {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} {J : TwoSidedIdeal R} :
        I = J ∀ (x : R), x I x J
        theorem TwoSidedIdeal.ext {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} {J : TwoSidedIdeal R} (h : ∀ (x : R), x I x J) :
        I = J
        theorem TwoSidedIdeal.lt_iff {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (J : TwoSidedIdeal R) :
        I < J I J
        theorem TwoSidedIdeal.add_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x : R} {y : R} (hx : x I) (hy : y I) :
        x + y I
        theorem TwoSidedIdeal.neg_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x : R} (hx : x I) :
        -x I
        theorem TwoSidedIdeal.sub_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x : R} {y : R} (hx : x I) (hy : y I) :
        x - y I
        theorem TwoSidedIdeal.mul_mem_left {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (x : R) (y : R) (hy : y I) :
        x * y I
        theorem TwoSidedIdeal.mul_mem_right {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (x : R) (y : R) (hx : x I) :
        x * y I
        theorem TwoSidedIdeal.nsmul_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x : R} (n : ) (hx : x I) :
        n x I
        theorem TwoSidedIdeal.zsmul_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x : R} (n : ) (hx : x I) :
        n x I
        def TwoSidedIdeal.mk' {R : Type u_1} [NonUnitalNonAssocRing R] (carrier : Set R) (zero_mem : 0 carrier) (add_mem : ∀ {x y : R}, x carriery carrierx + y carrier) (neg_mem : ∀ {x : R}, x carrier-x carrier) (mul_mem_left : ∀ {x y : R}, y carrierx * y carrier) (mul_mem_right : ∀ {x y : R}, x carrierx * y carrier) :

        The "set-theoretic-way" of constructing a two-sided ideal by providing:

        • the underlying set S;
        • a proof that 0 ∈ S;
        • a proof that x + y ∈ S if x ∈ S and y ∈ S;
        • a proof that -x ∈ S if x ∈ S;
        • a proof that x * y ∈ S if y ∈ S;
        • a proof that x * y ∈ S if x ∈ S.
        Equations
        • TwoSidedIdeal.mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right = { ringCon := { r := fun (x y : R) => x - y carrier, iseqv := , mul' := , add' := } }
        Instances For
          @[simp]
          theorem TwoSidedIdeal.mem_mk' {R : Type u_1} [NonUnitalNonAssocRing R] (carrier : Set R) (zero_mem : 0 carrier) (add_mem : ∀ {x y : R}, x carriery carrierx + y carrier) (neg_mem : ∀ {x : R}, x carrier-x carrier) (mul_mem_left : ∀ {x y : R}, y carrierx * y carrier) (mul_mem_right : ∀ {x y : R}, x carrierx * y carrier) (x : R) :
          x TwoSidedIdeal.mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right x carrier
          @[simp]
          theorem TwoSidedIdeal.coe_mk' {R : Type u_1} [NonUnitalNonAssocRing R] (carrier : Set R) (zero_mem : 0 carrier) (add_mem : ∀ {x y : R}, x carriery carrierx + y carrier) (neg_mem : ∀ {x : R}, x carrier-x carrier) (mul_mem_left : ∀ {x y : R}, y carrierx * y carrier) (mul_mem_right : ∀ {x y : R}, x carrierx * y carrier) :
          (TwoSidedIdeal.mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right) = carrier
          Equations
          • I.instAddSubtypeMem = { add := fun (x y : I) => x + y, }
          Equations
          • I.instZeroSubtypeMem = { zero := 0, }
          Equations
          • I.instSMulNatSubtypeMem = { smul := fun (n : ) (x : I) => n x, }
          Equations
          • I.instNegSubtypeMem = { neg := fun (x : I) => -x, }
          Equations
          • I.instSubSubtypeMem = { sub := fun (x y : I) => x - y, }
          Equations
          • I.instSMulIntSubtypeMem = { smul := fun (n : ) (x : I) => n x, }
          Equations

          The coercion into the ring as a AddMonoidHom

          Equations
          • I.coeAddMonoidHom = { toFun := Subtype.val, map_zero' := , map_add' := }
          Instances For
            instance TwoSidedIdeal.instSMulSubtypeMem {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) :
            SMul R I
            Equations
            • I.instSMulSubtypeMem = { smul := fun (r : R) (x : I) => r x, }
            Equations
            • I.instSMulMulOppositeSubtypeMem = { smul := fun (r : Rᵐᵒᵖ) (x : I) => r x, }
            instance TwoSidedIdeal.leftModule {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) :
            Module R I
            Equations
            @[simp]
            theorem TwoSidedIdeal.coe_smul {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) {r : R} {x : I} :
            r x = r * x
            instance TwoSidedIdeal.rightModule {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) :
            Equations
            @[simp]
            theorem TwoSidedIdeal.coe_mop_smul {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) {r : Rᵐᵒᵖ} {x : I} :
            r x = x * MulOpposite.unop r
            @[simp]
            theorem TwoSidedIdeal.subtype_apply {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) (x : I) :
            I.subtype x = x
            def TwoSidedIdeal.subtype {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) :
            I →ₗ[R] R

            For any I : RingCon R, when we view it as an ideal, I.subtype is the injective R-linear map I → R.

            Equations
            • I.subtype = { toFun := fun (x : I) => x, map_add' := , map_smul' := }
            Instances For
              @[simp]
              theorem TwoSidedIdeal.subtypeMop_apply {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) (x : I) :
              I.subtypeMop x = MulOpposite.op x

              For any RingCon R, when we view it as an ideal in Rᵒᵖ, subtype is the injective Rᵐᵒᵖ-linear map I → Rᵐᵒᵖ.

              Equations
              • I.subtypeMop = { toFun := fun (x : I) => MulOpposite.op x, map_add' := , map_smul' := }
              Instances For