Documentation

Mathlib.Algebra.Group.Subgroup.MulOpposite

Mul-opposite subgroups #

Tags #

subgroup, subgroups

source
def Subgroup.op {G : Type u_1} [Group G] (H : Subgroup G) :
Subgroup Gᵐᵒᵖ

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

Instances For
    source
    def AddSubgroup.op {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
    AddSubgroup Gᵃᵒᵖ

    Pull an additive subgroup back to an opposite additive subgroup along AddOpposite.unop

    Instances For
      source
      @[simp]
      theorem Subgroup.coe_op {G : Type u_1} [Group G] (H : Subgroup G) :
      ↑H.op = MulOpposite.unop ⁻¹' ↑H
      source
      @[simp]
      theorem AddSubgroup.coe_op {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
      ↑H.op = AddOpposite.unop ⁻¹' ↑H
      source
      @[simp]
      theorem Subgroup.mem_op {G : Type u_1} [Group G] {x : Gᵐᵒᵖ} {S : Subgroup G} :
      x ∈ S.op ↔ MulOpposite.unop x ∈ S
      source
      @[simp]
      theorem AddSubgroup.mem_op {G : Type u_1} [AddGroup G] {x : Gᵃᵒᵖ} {S : AddSubgroup G} :
      x ∈ S.op ↔ AddOpposite.unop x ∈ S
      source
      @[simp]
      theorem Subgroup.op_toSubmonoid {G : Type u_1} [Group G] (H : Subgroup G) :
      H.op.toSubmonoid = H.op
      source
      @[simp]
      theorem AddSubgroup.op_toAddSubmonoid {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
      H.op.toAddSubmonoid = H.op
      source
      theorem Subgroup.op_toSubsemigroup {G : Type u_1} [Group G] (H : Subgroup G) :
      H.op.toSubsemigroup = H.op
      source
      theorem AddSubgroup.op_toSubsemigroup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
      H.op.toAddSubsemigroup = H.op
      source
      def Subgroup.unop {G : Type u_1} [Group G] (H : Subgroup Gᵐᵒᵖ) :
      Subgroup G

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

      Instances For
        source
        def AddSubgroup.unop {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
        AddSubgroup G

        Pull an opposite additive subgroup back to an additive subgroup along AddOpposite.op

        Instances For
          source
          @[simp]
          theorem AddSubgroup.coe_unop {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
          ↑H.unop = AddOpposite.op ⁻¹' ↑H
          source
          @[simp]
          theorem Subgroup.coe_unop {G : Type u_1} [Group G] (H : Subgroup Gᵐᵒᵖ) :
          ↑H.unop = MulOpposite.op ⁻¹' ↑H
          source
          @[simp]
          theorem Subgroup.mem_unop {G : Type u_1} [Group G] {x : G} {S : Subgroup Gᵐᵒᵖ} :
          x ∈ S.unop ↔ MulOpposite.op x ∈ S
          source
          @[simp]
          theorem AddSubgroup.mem_unop {G : Type u_1} [AddGroup G] {x : G} {S : AddSubgroup Gᵃᵒᵖ} :
          x ∈ S.unop ↔ AddOpposite.op x ∈ S
          source
          @[simp]
          theorem Subgroup.unop_toSubmonoid {G : Type u_1} [Group G] (H : Subgroup Gᵐᵒᵖ) :
          H.unop.toSubmonoid = H.unop
          source
          @[simp]
          theorem AddSubgroup.unop_toAddSubmonoid {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
          H.unop.toAddSubmonoid = H.unop
          source
          theorem Subgroup.unop_toSubsemigroup {G : Type u_1} [Group G] (H : Subgroup Gᵐᵒᵖ) :
          H.unop.toSubsemigroup = H.unop
          source
          theorem AddSubgroup.unop_toSubsemigroup {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
          H.unop.toAddSubsemigroup = H.unop
          source
          @[simp]
          theorem Subgroup.unop_op {G : Type u_1} [Group G] (S : Subgroup G) :
          S.op.unop = S
          source
          @[simp]
          theorem AddSubgroup.unop_op {G : Type u_1} [AddGroup G] (S : AddSubgroup G) :
          S.op.unop = S
          source
          @[simp]
          theorem Subgroup.op_unop {G : Type u_1} [Group G] (S : Subgroup Gᵐᵒᵖ) :
          S.unop.op = S
          source
          @[simp]
          theorem AddSubgroup.op_unop {G : Type u_1} [AddGroup G] (S : AddSubgroup Gᵃᵒᵖ) :
          S.unop.op = S

          Lattice results #

          source
          theorem Subgroup.op_le_iff {G : Type u_1} [Group G] {S₁ : Subgroup G} {S₂ : Subgroup Gᵐᵒᵖ} :
          S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
          source
          theorem AddSubgroup.op_le_iff {G : Type u_1} [AddGroup G] {S₁ : AddSubgroup G} {S₂ : AddSubgroup Gᵃᵒᵖ} :
          S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
          source
          theorem Subgroup.le_op_iff {G : Type u_1} [Group G] {S₁ : Subgroup Gᵐᵒᵖ} {S₂ : Subgroup G} :
          S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
          source
          theorem AddSubgroup.le_op_iff {G : Type u_1} [AddGroup G] {S₁ : AddSubgroup Gᵃᵒᵖ} {S₂ : AddSubgroup G} :
          S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
          source
          @[simp]
          theorem Subgroup.op_le_op_iff {G : Type u_1} [Group G] {S₁ S₂ : Subgroup G} :
          S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
          source
          @[simp]
          theorem AddSubgroup.op_le_op_iff {G : Type u_1} [AddGroup G] {S₁ S₂ : AddSubgroup G} :
          S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
          source
          @[simp]
          theorem Subgroup.unop_le_unop_iff {G : Type u_1} [Group G] {S₁ S₂ : Subgroup Gᵐᵒᵖ} :
          S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
          source
          @[simp]
          theorem AddSubgroup.unop_le_unop_iff {G : Type u_1} [AddGroup G] {S₁ S₂ : AddSubgroup Gᵃᵒᵖ} :
          S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
          source
          def Subgroup.opEquiv {G : Type u_1} [Group G] :
          Subgroup G ≃o Subgroup Gᵐᵒᵖ

          A subgroup H of G determines a subgroup H.op of the opposite group Gᵐᵒᵖ.

          Instances For
            source
            def AddSubgroup.opEquiv {G : Type u_1} [AddGroup G] :
            AddSubgroup G ≃o AddSubgroup Gᵃᵒᵖ

            An additive subgroup H of G determines an additive subgroup H.op of the opposite additive group Gᵃᵒᵖ.

            Instances For
              source
              @[simp]
              theorem Subgroup.opEquiv_apply {G : Type u_1} [Group G] (H : Subgroup G) :
              opEquiv H = H.op
              source
              @[simp]
              theorem AddSubgroup.opEquiv_symm_apply {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
              (RelIso.symm opEquiv) H = H.unop
              source
              @[simp]
              theorem Subgroup.opEquiv_symm_apply {G : Type u_1} [Group G] (H : Subgroup Gᵐᵒᵖ) :
              (RelIso.symm opEquiv) H = H.unop
              source
              @[simp]
              theorem AddSubgroup.opEquiv_apply {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
              opEquiv H = H.op
              source
              theorem Subgroup.op_injective {G : Type u_1} [Group G] :
              Function.Injective Subgroup.op
              source
              theorem AddSubgroup.op_injective {G : Type u_1} [AddGroup G] :
              Function.Injective AddSubgroup.op
              source
              theorem Subgroup.unop_injective {G : Type u_1} [Group G] :
              Function.Injective Subgroup.unop
              source
              theorem AddSubgroup.unop_injective {G : Type u_1} [AddGroup G] :
              Function.Injective AddSubgroup.unop
              source
              @[simp]
              theorem Subgroup.op_inj {G : Type u_1} [Group G] {S T : Subgroup G} :
              S.op = T.op ↔ S = T
              source
              @[simp]
              theorem AddSubgroup.op_inj {G : Type u_1} [AddGroup G] {S T : AddSubgroup G} :
              S.op = T.op ↔ S = T
              source
              @[simp]
              theorem Subgroup.unop_inj {G : Type u_1} [Group G] {S T : Subgroup Gᵐᵒᵖ} :
              S.unop = T.unop ↔ S = T
              source
              @[simp]
              theorem AddSubgroup.unop_inj {G : Type u_1} [AddGroup G] {S T : AddSubgroup Gᵃᵒᵖ} :
              S.unop = T.unop ↔ S = T
              source
              def Subgroup.equivOp {G : Type u_1} [Group G] (H : Subgroup G) :
              ↥H ≃ ↥H.op

              Bijection between a subgroup H and its opposite.

              Instances For
                source
                def AddSubgroup.equivOp {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                ↥H ≃ ↥H.op

                Bijection between an additive subgroup H and its opposite.

                Instances For
                  source
                  @[simp]
                  theorem Subgroup.equivOp_apply_coe {G : Type u_1} [Group G] (H : Subgroup G) (a : ↥H) :
                  ↑(H.equivOp a) = MulOpposite.op ↑a
                  source
                  @[simp]
                  theorem AddSubgroup.equivOp_apply_coe {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (a : ↥H) :
                  ↑(H.equivOp a) = AddOpposite.op ↑a
                  source
                  @[simp]
                  theorem Subgroup.equivOp_symm_apply_coe {G : Type u_1} [Group G] (H : Subgroup G) (b : ↥H.op) :
                  ↑(H.equivOp.symm b) = MulOpposite.unop ↑b
                  source
                  @[simp]
                  theorem AddSubgroup.equivOp_symm_apply_coe {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (b : ↥H.op) :
                  ↑(H.equivOp.symm b) = AddOpposite.unop ↑b
                  source
                  theorem Subgroup.op_normalizer {G : Type u_1} [Group G] (H : Subgroup G) :
                  (normalizer ↑H).op = normalizer ↑H.op
                  source
                  theorem AddSubgroup.op_normalizer {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                  (normalizer ↑H).op = normalizer ↑H.op
                  source
                  theorem Subgroup.unop_normalizer {G : Type u_1} [Group G] (H : Subgroup Gᵐᵒᵖ) :
                  (normalizer ↑H).unop = normalizer ↑H.unop
                  source
                  theorem AddSubgroup.unop_normalizer {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
                  (normalizer ↑H).unop = normalizer ↑H.unop