Documentation

Mathlib.GroupTheory.Subgroup.MulOpposite

Mul-opposite subgroups #

Tags #

subgroup, subgroups

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

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

Equations
  • AddSubgroup.op H = { toAddSubmonoid := { toAddSubsemigroup := { carrier := AddOpposite.unop ⁻¹' ↑H, add_mem' := ⋯ }, zero_mem' := ⋯ }, neg_mem' := ⋯ }
Instances For
    source
    theorem AddSubgroup.op.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
    ∀ {a b : Gᵃᵒᵖ}, a ∈ AddOpposite.unop ⁻¹' ↑H → b ∈ AddOpposite.unop ⁻¹' ↑H → AddOpposite.unop b + AddOpposite.unop a ∈ H
    source
    theorem AddSubgroup.op.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
    ∀ {x : Gᵃᵒᵖ}, AddOpposite.unop x ∈ H → -AddOpposite.unop x ∈ H
    source
    @[simp]
    theorem AddSubgroup.op_coe {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
    ↑(AddSubgroup.op H) = AddOpposite.unop ⁻¹' ↑H
    source
    @[simp]
    theorem Subgroup.op_coe {G : Type u_2} [Group G] (H : Subgroup G) :
    ↑(Subgroup.op H) = MulOpposite.unop ⁻¹' ↑H
    source
    def Subgroup.op {G : Type u_2} [Group G] (H : Subgroup G) :
    Subgroup Gᵐᵒᵖ

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

    Equations
    • Subgroup.op H = { toSubmonoid := { toSubsemigroup := { carrier := MulOpposite.unop ⁻¹' ↑H, mul_mem' := ⋯ }, one_mem' := ⋯ }, inv_mem' := ⋯ }
    Instances For
      source
      @[simp]
      theorem AddSubgroup.mem_op {G : Type u_2} [AddGroup G] {x : Gᵃᵒᵖ} {S : AddSubgroup G} :
      x ∈ AddSubgroup.op S ↔ AddOpposite.unop x ∈ S
      source
      @[simp]
      theorem Subgroup.mem_op {G : Type u_2} [Group G] {x : Gᵐᵒᵖ} {S : Subgroup G} :
      x ∈ Subgroup.op S ↔ MulOpposite.unop x ∈ S
      source
      @[simp]
      theorem AddSubgroup.op_toAddSubmonoid {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
      (AddSubgroup.op H).toAddSubmonoid = AddSubmonoid.op H.toAddSubmonoid
      source
      @[simp]
      theorem Subgroup.op_toSubmonoid {G : Type u_2} [Group G] (H : Subgroup G) :
      (Subgroup.op H).toSubmonoid = Submonoid.op H.toSubmonoid
      source
      theorem AddSubgroup.unop.proof_3 {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
      ∀ {x : G}, AddOpposite.op x ∈ H → -AddOpposite.op x ∈ H
      source
      def AddSubgroup.unop {G : Type u_2} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
      AddSubgroup G

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

      Equations
      • AddSubgroup.unop H = { toAddSubmonoid := { toAddSubsemigroup := { carrier := AddOpposite.op ⁻¹' ↑H, add_mem' := ⋯ }, zero_mem' := ⋯ }, neg_mem' := ⋯ }
      Instances For
        source
        theorem AddSubgroup.unop.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
        ∀ {a b : G}, a ∈ AddOpposite.op ⁻¹' ↑H → b ∈ AddOpposite.op ⁻¹' ↑H → { unop' := b } + { unop' := a } ∈ H
        source
        theorem AddSubgroup.unop.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
        0 ∈ H
        source
        @[simp]
        theorem AddSubgroup.unop_coe {G : Type u_2} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
        ↑(AddSubgroup.unop H) = AddOpposite.op ⁻¹' ↑H
        source
        @[simp]
        theorem Subgroup.unop_coe {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) :
        ↑(Subgroup.unop H) = MulOpposite.op ⁻¹' ↑H
        source
        def Subgroup.unop {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) :
        Subgroup G

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

        Equations
        • Subgroup.unop H = { toSubmonoid := { toSubsemigroup := { carrier := MulOpposite.op ⁻¹' ↑H, mul_mem' := ⋯ }, one_mem' := ⋯ }, inv_mem' := ⋯ }
        Instances For
          source
          @[simp]
          theorem AddSubgroup.mem_unop {G : Type u_2} [AddGroup G] {x : G} {S : AddSubgroup Gᵃᵒᵖ} :
          x ∈ AddSubgroup.unop S ↔ AddOpposite.op x ∈ S
          source
          @[simp]
          theorem Subgroup.mem_unop {G : Type u_2} [Group G] {x : G} {S : Subgroup Gᵐᵒᵖ} :
          x ∈ Subgroup.unop S ↔ MulOpposite.op x ∈ S
          source
          @[simp]
          theorem AddSubgroup.unop_toAddSubmonoid {G : Type u_2} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
          (AddSubgroup.unop H).toAddSubmonoid = AddSubmonoid.unop H.toAddSubmonoid
          source
          @[simp]
          theorem Subgroup.unop_toSubmonoid {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) :
          (Subgroup.unop H).toSubmonoid = Submonoid.unop H.toSubmonoid
          source
          @[simp]
          theorem AddSubgroup.unop_op {G : Type u_2} [AddGroup G] (S : AddSubgroup G) :
          AddSubgroup.unop (AddSubgroup.op S) = S
          source
          @[simp]
          theorem Subgroup.unop_op {G : Type u_2} [Group G] (S : Subgroup G) :
          Subgroup.unop (Subgroup.op S) = S
          source
          @[simp]
          theorem AddSubgroup.op_unop {G : Type u_2} [AddGroup G] (S : AddSubgroup Gᵃᵒᵖ) :
          AddSubgroup.op (AddSubgroup.unop S) = S
          source
          @[simp]
          theorem Subgroup.op_unop {G : Type u_2} [Group G] (S : Subgroup Gᵐᵒᵖ) :
          Subgroup.op (Subgroup.unop S) = S

          Lattice results #

          source
          theorem AddSubgroup.op_le_iff {G : Type u_2} [AddGroup G] {S₁ : AddSubgroup G} {S₂ : AddSubgroup Gᵃᵒᵖ} :
          AddSubgroup.op S₁ ≤ S₂ ↔ S₁ ≤ AddSubgroup.unop S₂
          source
          theorem Subgroup.op_le_iff {G : Type u_2} [Group G] {S₁ : Subgroup G} {S₂ : Subgroup Gᵐᵒᵖ} :
          Subgroup.op S₁ ≤ S₂ ↔ S₁ ≤ Subgroup.unop S₂
          source
          theorem AddSubgroup.le_op_iff {G : Type u_2} [AddGroup G] {S₁ : AddSubgroup Gᵃᵒᵖ} {S₂ : AddSubgroup G} :
          S₁ ≤ AddSubgroup.op S₂ ↔ AddSubgroup.unop S₁ ≤ S₂
          source
          theorem Subgroup.le_op_iff {G : Type u_2} [Group G] {S₁ : Subgroup Gᵐᵒᵖ} {S₂ : Subgroup G} :
          S₁ ≤ Subgroup.op S₂ ↔ Subgroup.unop S₁ ≤ S₂
          source
          @[simp]
          theorem AddSubgroup.op_le_op_iff {G : Type u_2} [AddGroup G] {S₁ : AddSubgroup G} {S₂ : AddSubgroup G} :
          AddSubgroup.op S₁ ≤ AddSubgroup.op S₂ ↔ S₁ ≤ S₂
          source
          @[simp]
          theorem Subgroup.op_le_op_iff {G : Type u_2} [Group G] {S₁ : Subgroup G} {S₂ : Subgroup G} :
          Subgroup.op S₁ ≤ Subgroup.op S₂ ↔ S₁ ≤ S₂
          source
          @[simp]
          theorem AddSubgroup.unop_le_unop_iff {G : Type u_2} [AddGroup G] {S₁ : AddSubgroup Gᵃᵒᵖ} {S₂ : AddSubgroup Gᵃᵒᵖ} :
          AddSubgroup.unop S₁ ≤ AddSubgroup.unop S₂ ↔ S₁ ≤ S₂
          source
          @[simp]
          theorem Subgroup.unop_le_unop_iff {G : Type u_2} [Group G] {S₁ : Subgroup Gᵐᵒᵖ} {S₂ : Subgroup Gᵐᵒᵖ} :
          Subgroup.unop S₁ ≤ Subgroup.unop S₂ ↔ S₁ ≤ S₂
          source
          def AddSubgroup.opEquiv {G : Type u_2} [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ᵃᵒᵖ.

          Equations
          • AddSubgroup.opEquiv = { toEquiv := { toFun := AddSubgroup.op, invFun := AddSubgroup.unop, left_inv := ⋯, right_inv := ⋯ }, map_rel_iff' := ⋯ }
          Instances For
            source
            @[simp]
            theorem AddSubgroup.opEquiv_apply {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
            AddSubgroup.opEquiv H = AddSubgroup.op H
            source
            @[simp]
            theorem Subgroup.opEquiv_symm_apply {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) :
            (RelIso.symm Subgroup.opEquiv) H = Subgroup.unop H
            source
            @[simp]
            theorem Subgroup.opEquiv_apply {G : Type u_2} [Group G] (H : Subgroup G) :
            Subgroup.opEquiv H = Subgroup.op H
            source
            @[simp]
            theorem AddSubgroup.opEquiv_symm_apply {G : Type u_2} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
            (RelIso.symm AddSubgroup.opEquiv) H = AddSubgroup.unop H
            source
            def Subgroup.opEquiv {G : Type u_2} [Group G] :
            Subgroup G ≃o Subgroup Gᵐᵒᵖ

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

            Equations
            • Subgroup.opEquiv = { toEquiv := { toFun := Subgroup.op, invFun := Subgroup.unop, left_inv := ⋯, right_inv := ⋯ }, map_rel_iff' := ⋯ }
            Instances For
              source
              @[simp]
              theorem AddSubgroup.op_bot {G : Type u_2} [AddGroup G] :
              AddSubgroup.op ⊥ = ⊥
              source
              @[simp]
              theorem Subgroup.op_bot {G : Type u_2} [Group G] :
              Subgroup.op ⊥ = ⊥
              source
              @[simp]
              theorem AddSubgroup.unop_bot {G : Type u_2} [AddGroup G] :
              AddSubgroup.unop ⊥ = ⊥
              source
              @[simp]
              theorem Subgroup.unop_bot {G : Type u_2} [Group G] :
              Subgroup.unop ⊥ = ⊥
              source
              @[simp]
              theorem AddSubgroup.op_top {G : Type u_2} [AddGroup G] :
              AddSubgroup.op ⊤ = ⊤
              source
              @[simp]
              theorem Subgroup.op_top {G : Type u_2} [Group G] :
              Subgroup.op ⊤ = ⊤
              source
              @[simp]
              theorem AddSubgroup.unop_top {G : Type u_2} [AddGroup G] :
              AddSubgroup.unop ⊤ = ⊤
              source
              @[simp]
              theorem Subgroup.unop_top {G : Type u_2} [Group G] :
              Subgroup.unop ⊤ = ⊤
              source
              theorem AddSubgroup.op_sup {G : Type u_2} [AddGroup G] (S₁ : AddSubgroup G) (S₂ : AddSubgroup G) :
              AddSubgroup.op (S₁ ⊔ S₂) = AddSubgroup.op S₁ ⊔ AddSubgroup.op S₂
              source
              theorem Subgroup.op_sup {G : Type u_2} [Group G] (S₁ : Subgroup G) (S₂ : Subgroup G) :
              Subgroup.op (S₁ ⊔ S₂) = Subgroup.op S₁ ⊔ Subgroup.op S₂
              source
              theorem AddSubgroup.unop_sup {G : Type u_2} [AddGroup G] (S₁ : AddSubgroup Gᵃᵒᵖ) (S₂ : AddSubgroup Gᵃᵒᵖ) :
              AddSubgroup.unop (S₁ ⊔ S₂) = AddSubgroup.unop S₁ ⊔ AddSubgroup.unop S₂
              source
              theorem Subgroup.unop_sup {G : Type u_2} [Group G] (S₁ : Subgroup Gᵐᵒᵖ) (S₂ : Subgroup Gᵐᵒᵖ) :
              Subgroup.unop (S₁ ⊔ S₂) = Subgroup.unop S₁ ⊔ Subgroup.unop S₂
              source
              theorem AddSubgroup.op_inf {G : Type u_2} [AddGroup G] (S₁ : AddSubgroup G) (S₂ : AddSubgroup G) :
              AddSubgroup.op (S₁ ⊓ S₂) = AddSubgroup.op S₁ ⊓ AddSubgroup.op S₂
              source
              theorem Subgroup.op_inf {G : Type u_2} [Group G] (S₁ : Subgroup G) (S₂ : Subgroup G) :
              Subgroup.op (S₁ ⊓ S₂) = Subgroup.op S₁ ⊓ Subgroup.op S₂
              source
              theorem AddSubgroup.unop_inf {G : Type u_2} [AddGroup G] (S₁ : AddSubgroup Gᵃᵒᵖ) (S₂ : AddSubgroup Gᵃᵒᵖ) :
              AddSubgroup.unop (S₁ ⊓ S₂) = AddSubgroup.unop S₁ ⊓ AddSubgroup.unop S₂
              source
              theorem Subgroup.unop_inf {G : Type u_2} [Group G] (S₁ : Subgroup Gᵐᵒᵖ) (S₂ : Subgroup Gᵐᵒᵖ) :
              Subgroup.unop (S₁ ⊓ S₂) = Subgroup.unop S₁ ⊓ Subgroup.unop S₂
              source
              theorem AddSubgroup.op_sSup {G : Type u_2} [AddGroup G] (S : Set (AddSubgroup G)) :
              AddSubgroup.op (sSup S) = sSup (AddSubgroup.unop ⁻¹' S)
              source
              theorem Subgroup.op_sSup {G : Type u_2} [Group G] (S : Set (Subgroup G)) :
              Subgroup.op (sSup S) = sSup (Subgroup.unop ⁻¹' S)
              source
              theorem AddSubgroup.unop_sSup {G : Type u_2} [AddGroup G] (S : Set (AddSubgroup Gᵃᵒᵖ)) :
              AddSubgroup.unop (sSup S) = sSup (AddSubgroup.op ⁻¹' S)
              source
              theorem Subgroup.unop_sSup {G : Type u_2} [Group G] (S : Set (Subgroup Gᵐᵒᵖ)) :
              Subgroup.unop (sSup S) = sSup (Subgroup.op ⁻¹' S)
              source
              theorem AddSubgroup.op_sInf {G : Type u_2} [AddGroup G] (S : Set (AddSubgroup G)) :
              AddSubgroup.op (sInf S) = sInf (AddSubgroup.unop ⁻¹' S)
              source
              theorem Subgroup.op_sInf {G : Type u_2} [Group G] (S : Set (Subgroup G)) :
              Subgroup.op (sInf S) = sInf (Subgroup.unop ⁻¹' S)
              source
              theorem AddSubgroup.unop_sInf {G : Type u_2} [AddGroup G] (S : Set (AddSubgroup Gᵃᵒᵖ)) :
              AddSubgroup.unop (sInf S) = sInf (AddSubgroup.op ⁻¹' S)
              source
              theorem Subgroup.unop_sInf {G : Type u_2} [Group G] (S : Set (Subgroup Gᵐᵒᵖ)) :
              Subgroup.unop (sInf S) = sInf (Subgroup.op ⁻¹' S)
              source
              theorem AddSubgroup.op_iSup {ι : Sort u_1} {G : Type u_2} [AddGroup G] (S : ι → AddSubgroup G) :
              AddSubgroup.op (iSup S) = ⨆ (i : ι), AddSubgroup.op (S i)
              source
              theorem Subgroup.op_iSup {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup G) :
              Subgroup.op (iSup S) = ⨆ (i : ι), Subgroup.op (S i)
              source
              theorem AddSubgroup.unop_iSup {ι : Sort u_1} {G : Type u_2} [AddGroup G] (S : ι → AddSubgroup Gᵃᵒᵖ) :
              AddSubgroup.unop (iSup S) = ⨆ (i : ι), AddSubgroup.unop (S i)
              source
              theorem Subgroup.unop_iSup {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup Gᵐᵒᵖ) :
              Subgroup.unop (iSup S) = ⨆ (i : ι), Subgroup.unop (S i)
              source
              theorem AddSubgroup.op_iInf {ι : Sort u_1} {G : Type u_2} [AddGroup G] (S : ι → AddSubgroup G) :
              AddSubgroup.op (iInf S) = ⨅ (i : ι), AddSubgroup.op (S i)
              source
              theorem Subgroup.op_iInf {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup G) :
              Subgroup.op (iInf S) = ⨅ (i : ι), Subgroup.op (S i)
              source
              theorem AddSubgroup.unop_iInf {ι : Sort u_1} {G : Type u_2} [AddGroup G] (S : ι → AddSubgroup Gᵃᵒᵖ) :
              AddSubgroup.unop (iInf S) = ⨅ (i : ι), AddSubgroup.unop (S i)
              source
              theorem Subgroup.unop_iInf {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup Gᵐᵒᵖ) :
              Subgroup.unop (iInf S) = ⨅ (i : ι), Subgroup.unop (S i)
              source
              theorem AddSubgroup.op_closure {G : Type u_2} [AddGroup G] (s : Set G) :
              AddSubgroup.op (AddSubgroup.closure s) = AddSubgroup.closure (AddOpposite.unop ⁻¹' s)
              source
              theorem Subgroup.op_closure {G : Type u_2} [Group G] (s : Set G) :
              Subgroup.op (Subgroup.closure s) = Subgroup.closure (MulOpposite.unop ⁻¹' s)
              source
              theorem AddSubgroup.unop_closure {G : Type u_2} [AddGroup G] (s : Set Gᵃᵒᵖ) :
              AddSubgroup.unop (AddSubgroup.closure s) = AddSubgroup.closure (AddOpposite.op ⁻¹' s)
              source
              theorem Subgroup.unop_closure {G : Type u_2} [Group G] (s : Set Gᵐᵒᵖ) :
              Subgroup.unop (Subgroup.closure s) = Subgroup.closure (MulOpposite.op ⁻¹' s)
              source
              theorem AddSubgroup.equivOp.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
              ∀ (x : G), x ∈ H ↔ x ∈ H
              source
              def AddSubgroup.equivOp {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
              ↥H ≃ ↥(AddSubgroup.op H)

              Bijection between an additive subgroup H and its opposite.

              Equations
              Instances For
                source
                @[simp]
                theorem Subgroup.equivOp_apply_coe {G : Type u_2} [Group G] (H : Subgroup G) (a : { a : G // (fun (x : G) => x ∈ H) a }) :
                ↑((Subgroup.equivOp H) a) = MulOpposite.op ↑a
                source
                @[simp]
                theorem AddSubgroup.equivOp_apply_coe {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (a : { a : G // (fun (x : G) => x ∈ H) a }) :
                ↑((AddSubgroup.equivOp H) a) = AddOpposite.op ↑a
                source
                @[simp]
                theorem Subgroup.equivOp_symm_apply_coe {G : Type u_2} [Group G] (H : Subgroup G) (b : { b : Gᵐᵒᵖ // (fun (x : Gᵐᵒᵖ) => x ∈ Subgroup.op H) b }) :
                ↑((Subgroup.equivOp H).symm b) = MulOpposite.unop ↑b
                source
                @[simp]
                theorem AddSubgroup.equivOp_symm_apply_coe {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (b : { b : Gᵃᵒᵖ // (fun (x : Gᵃᵒᵖ) => x ∈ AddSubgroup.op H) b }) :
                ↑((AddSubgroup.equivOp H).symm b) = AddOpposite.unop ↑b
                source
                def Subgroup.equivOp {G : Type u_2} [Group G] (H : Subgroup G) :
                ↥H ≃ ↥(Subgroup.op H)

                Bijection between a subgroup H and its opposite.

                Equations
                Instances For
                  source
                  instance AddSubgroup.instEncodableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupOp {G : Type u_2} [AddGroup G] (H : AddSubgroup G) [Encodable ↥H] :
                  Encodable ↥(AddSubgroup.op H)
                  Equations
                  source
                  instance Subgroup.instEncodableSubtypeMulOppositeMemSubgroupGroupInstMembershipInstSetLikeSubgroupOp {G : Type u_2} [Group G] (H : Subgroup G) [Encodable ↥H] :
                  Encodable ↥(Subgroup.op H)
                  Equations
                  source
                  instance AddSubgroup.instCountableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupOp {G : Type u_2} [AddGroup G] (H : AddSubgroup G) [Countable ↥H] :
                  Countable ↥(AddSubgroup.op H)
                  Equations
                  • ⋯ = ⋯
                  source
                  instance Subgroup.instCountableSubtypeMulOppositeMemSubgroupGroupInstMembershipInstSetLikeSubgroupOp {G : Type u_2} [Group G] (H : Subgroup G) [Countable ↥H] :
                  Countable ↥(Subgroup.op H)
                  Equations
                  • ⋯ = ⋯
                  source
                  theorem AddSubgroup.vadd_opposite_add {G : Type u_2} [AddGroup G] {H : AddSubgroup G} (x : G) (g : G) (h : ↥(AddSubgroup.op H)) :
                  h +ᵥ (g + x) = g + (h +ᵥ x)
                  source
                  theorem Subgroup.smul_opposite_mul {G : Type u_2} [Group G] {H : Subgroup G} (x : G) (g : G) (h : ↥(Subgroup.op H)) :
                  h • (g * x) = g * h • x