Mul-opposite subgroups

This file contains a somewhat arbitrary assortment of results on the opposite subgroup H.op that rely on further theory to define. As such it is a somewhat arbitrary assortment of results, which might be organized and split up further.

Tags

subgroup, subgroups

@[implicit_reducible]

instance Subgroup.instSMul {G : Type u_2} [Group G] (H : Subgroup G) : SMul (↥H.op) G

We redeclare this instance to get keys SMul (@Subtype (MulOpposite _) (@Membership.mem (MulOpposite _) (Subgroup (MulOpposite _) _) _ (@Subgroup.op _ _ _))) _ compared to the keys for Submonoid.smul SMul (@Subtype _ (@Membership.mem _ (Submonoid _ _) _ _)) _

Equations

• H.instSMul = H.op.smul

@[implicit_reducible]

instance AddSubgroup.instVAdd {G : Type u_2} [AddGroup G] (H : AddSubgroup G) : VAdd (↥H.op) G

Equations

• H.instVAdd = H.op.vadd

Lattice results

@[simp]

theorem Subgroup.op_bot {G : Type u_2} [Group G] : ⊥.op = ⊥

@[simp]

theorem AddSubgroup.op_bot {G : Type u_2} [AddGroup G] : ⊥.op = ⊥

@[simp]

theorem Subgroup.op_eq_bot {G : Type u_2} [Group G] {S : Subgroup G} : S.op = ⊥ ↔ S = ⊥

@[simp]

theorem AddSubgroup.op_eq_bot {G : Type u_2} [AddGroup G] {S : AddSubgroup G} : S.op = ⊥ ↔ S = ⊥

@[simp]

theorem Subgroup.unop_bot {G : Type u_2} [Group G] : ⊥.unop = ⊥

@[simp]

theorem AddSubgroup.unop_bot {G : Type u_2} [AddGroup G] : ⊥.unop = ⊥

@[simp]

theorem Subgroup.unop_eq_bot {G : Type u_2} [Group G] {S : Subgroup Gᵐᵒᵖ} : S.unop = ⊥ ↔ S = ⊥

@[simp]

theorem AddSubgroup.unop_eq_bot {G : Type u_2} [AddGroup G] {S : AddSubgroup Gᵃᵒᵖ} : S.unop = ⊥ ↔ S = ⊥

@[simp]

theorem Subgroup.op_top {G : Type u_2} [Group G] : ⊤.op = ⊤

@[simp]

theorem AddSubgroup.op_top {G : Type u_2} [AddGroup G] : ⊤.op = ⊤

@[simp]

theorem Subgroup.op_eq_top {G : Type u_2} [Group G] {S : Subgroup G} : S.op = ⊤ ↔ S = ⊤

@[simp]

theorem AddSubgroup.op_eq_top {G : Type u_2} [AddGroup G] {S : AddSubgroup G} : S.op = ⊤ ↔ S = ⊤

@[simp]

theorem Subgroup.unop_top {G : Type u_2} [Group G] : ⊤.unop = ⊤

@[simp]

theorem AddSubgroup.unop_top {G : Type u_2} [AddGroup G] : ⊤.unop = ⊤

@[simp]

theorem Subgroup.unop_eq_top {G : Type u_2} [Group G] {S : Subgroup Gᵐᵒᵖ} : S.unop = ⊤ ↔ S = ⊤

@[simp]

theorem AddSubgroup.unop_eq_top {G : Type u_2} [AddGroup G] {S : AddSubgroup Gᵃᵒᵖ} : S.unop = ⊤ ↔ S = ⊤

theorem Subgroup.op_sup {G : Type u_2} [Group G] (S₁ S₂ : Subgroup G) : (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op

theorem AddSubgroup.op_sup {G : Type u_2} [AddGroup G] (S₁ S₂ : AddSubgroup G) : (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op

theorem Subgroup.unop_sup {G : Type u_2} [Group G] (S₁ S₂ : Subgroup Gᵐᵒᵖ) : (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop

theorem AddSubgroup.unop_sup {G : Type u_2} [AddGroup G] (S₁ S₂ : AddSubgroup Gᵃᵒᵖ) : (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop

theorem Subgroup.op_inf {G : Type u_2} [Group G] (S₁ S₂ : Subgroup G) : (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op

theorem AddSubgroup.op_inf {G : Type u_2} [AddGroup G] (S₁ S₂ : AddSubgroup G) : (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op

theorem Subgroup.unop_inf {G : Type u_2} [Group G] (S₁ S₂ : Subgroup Gᵐᵒᵖ) : (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop

theorem AddSubgroup.unop_inf {G : Type u_2} [AddGroup G] (S₁ S₂ : AddSubgroup Gᵃᵒᵖ) : (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop

theorem Subgroup.op_sSup {G : Type u_2} [Group G] (S : Set (Subgroup G)) : (sSup S).op = sSup (Subgroup.unop ⁻¹' S)

theorem AddSubgroup.op_sSup {G : Type u_2} [AddGroup G] (S : Set (AddSubgroup G)) : (sSup S).op = sSup (AddSubgroup.unop ⁻¹' S)

theorem Subgroup.unop_sSup {G : Type u_2} [Group G] (S : Set (Subgroup Gᵐᵒᵖ)) : (sSup S).unop = sSup (Subgroup.op ⁻¹' S)

theorem AddSubgroup.unop_sSup {G : Type u_2} [AddGroup G] (S : Set (AddSubgroup Gᵃᵒᵖ)) : (sSup S).unop = sSup (AddSubgroup.op ⁻¹' S)

theorem Subgroup.op_sInf {G : Type u_2} [Group G] (S : Set (Subgroup G)) : (sInf S).op = sInf (Subgroup.unop ⁻¹' S)

theorem AddSubgroup.op_sInf {G : Type u_2} [AddGroup G] (S : Set (AddSubgroup G)) : (sInf S).op = sInf (AddSubgroup.unop ⁻¹' S)

theorem Subgroup.unop_sInf {G : Type u_2} [Group G] (S : Set (Subgroup Gᵐᵒᵖ)) : (sInf S).unop = sInf (Subgroup.op ⁻¹' S)

theorem AddSubgroup.unop_sInf {G : Type u_2} [AddGroup G] (S : Set (AddSubgroup Gᵃᵒᵖ)) : (sInf S).unop = sInf (AddSubgroup.op ⁻¹' S)

theorem Subgroup.op_iSup {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup G) : (iSup S).op = ⨆ (i : ι), (S i).op

theorem AddSubgroup.op_iSup {ι : Sort u_1} {G : Type u_2} [AddGroup G] (S : ι → AddSubgroup G) : (iSup S).op = ⨆ (i : ι), (S i).op

theorem Subgroup.unop_iSup {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup Gᵐᵒᵖ) : (iSup S).unop = ⨆ (i : ι), (S i).unop

theorem AddSubgroup.unop_iSup {ι : Sort u_1} {G : Type u_2} [AddGroup G] (S : ι → AddSubgroup Gᵃᵒᵖ) : (iSup S).unop = ⨆ (i : ι), (S i).unop

theorem Subgroup.op_iInf {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup G) : (iInf S).op = ⨅ (i : ι), (S i).op

theorem AddSubgroup.op_iInf {ι : Sort u_1} {G : Type u_2} [AddGroup G] (S : ι → AddSubgroup G) : (iInf S).op = ⨅ (i : ι), (S i).op

theorem Subgroup.unop_iInf {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup Gᵐᵒᵖ) : (iInf S).unop = ⨅ (i : ι), (S i).unop

theorem AddSubgroup.unop_iInf {ι : Sort u_1} {G : Type u_2} [AddGroup G] (S : ι → AddSubgroup Gᵃᵒᵖ) : (iInf S).unop = ⨅ (i : ι), (S i).unop

theorem Subgroup.op_closure {G : Type u_2} [Group G] (s : Set G) : (closure s).op = closure (MulOpposite.unop ⁻¹' s)

theorem AddSubgroup.op_closure {G : Type u_2} [AddGroup G] (s : Set G) : (closure s).op = closure (AddOpposite.unop ⁻¹' s)

theorem Subgroup.unop_closure {G : Type u_2} [Group G] (s : Set Gᵐᵒᵖ) : (closure s).unop = closure (MulOpposite.op ⁻¹' s)

theorem AddSubgroup.unop_closure {G : Type u_2} [AddGroup G] (s : Set Gᵃᵒᵖ) : (closure s).unop = closure (AddOpposite.op ⁻¹' s)

@[implicit_reducible]

instance Subgroup.instEncodableSubtypeMulOppositeMemOp {G : Type u_2} [Group G] (H : Subgroup G) [Encodable ↥H] : Encodable ↥H.op

Equations

• H.instEncodableSubtypeMulOppositeMemOp = Encodable.ofEquiv (↥H) H.equivOp.symm

@[implicit_reducible]

instance AddSubgroup.instEncodableSubtypeAddOppositeMemOp {G : Type u_2} [AddGroup G] (H : AddSubgroup G) [Encodable ↥H] : Encodable ↥H.op

Equations

• H.instEncodableSubtypeAddOppositeMemOp = Encodable.ofEquiv (↥H) H.equivOp.symm

instance Subgroup.instCountableSubtypeMulOppositeMemOp {G : Type u_2} [Group G] (H : Subgroup G) [Countable ↥H] : Countable ↥H.op

instance AddSubgroup.instCountableSubtypeAddOppositeMemOp {G : Type u_2} [AddGroup G] (H : AddSubgroup G) [Countable ↥H] : Countable ↥H.op

theorem Subgroup.smul_opposite_mul {G : Type u_2} [Group G] {H : Subgroup G} (x g : G) (h : ↥H.op) : h • (g * x) = g * h • x

theorem AddSubgroup.vadd_opposite_add {G : Type u_2} [AddGroup G] {H : AddSubgroup G} (x g : G) (h : ↥H.op) : h +ᵥ g + x = g + (h +ᵥ x)

@[simp]

theorem Subgroup.normal_op {G : Type u_2} [Group G] {H : Subgroup G} : H.op.Normal ↔ H.Normal

@[simp]

theorem AddSubgroup.normal_op {G : Type u_2} [AddGroup G] {H : AddSubgroup G} : H.op.Normal ↔ H.Normal

theorem Subgroup.Normal.of_op {G : Type u_2} [Group G] {H : Subgroup G} : H.op.Normal → H.Normal

Alias of the forward direction of Subgroup.normal_op.

theorem Subgroup.Normal.op {G : Type u_2} [Group G] {H : Subgroup G} : H.Normal → H.op.Normal

Alias of the reverse direction of Subgroup.normal_op.

theorem AddSubgroup.Normal.of_op {G : Type u_2} [AddGroup G] {H : AddSubgroup G} : H.op.Normal → H.Normal

theorem AddSubgroup.Normal.op {G : Type u_2} [AddGroup G] {H : AddSubgroup G} : H.Normal → H.op.Normal

instance Subgroup.op.instNormal {G : Type u_2} [Group G] {H : Subgroup G} [H.Normal] : H.op.Normal

instance AddSubgroup.op.instNormal {G : Type u_2} [AddGroup G] {H : AddSubgroup G} [H.Normal] : H.op.Normal

@[simp]

theorem Subgroup.normal_unop {G : Type u_2} [Group G] {H : Subgroup Gᵐᵒᵖ} : H.unop.Normal ↔ H.Normal

@[simp]

theorem AddSubgroup.normal_unop {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} : H.unop.Normal ↔ H.Normal

theorem Subgroup.Normal.of_unop {G : Type u_2} [Group G] {H : Subgroup Gᵐᵒᵖ} : H.unop.Normal → H.Normal

Alias of the forward direction of Subgroup.normal_unop.

theorem Subgroup.Normal.unop {G : Type u_2} [Group G] {H : Subgroup Gᵐᵒᵖ} : H.Normal → H.unop.Normal

Alias of the reverse direction of Subgroup.normal_unop.

theorem AddSubgroup.Normal.unop {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} : H.Normal → H.unop.Normal

theorem AddSubgroup.Normal.of_unop {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} : H.unop.Normal → H.Normal

instance Subgroup.unop.instNormal {G : Type u_2} [Group G] {H : Subgroup Gᵐᵒᵖ} [H.Normal] : H.unop.Normal

instance AddSubgroup.unop.instNormal {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} [H.Normal] : H.unop.Normal