Mul-opposite subgroups

Tags

subgroup, subgroups

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

• One or more equations did not get rendered due to their size.

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

theorem AddSubgroup.op.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ∀ {x : Gᵃᵒᵖ}, AddOpposite.unop x ∈ H → -AddOpposite.unop x ∈ H

@[simp]

theorem AddSubgroup.op_coe {G : Type u_2} [AddGroup G] (H : AddSubgroup G) : ↑(AddSubgroup.op H) = AddOpposite.unop ⁻¹' ↑H

@[simp]

theorem Subgroup.op_coe {G : Type u_2} [Group G] (H : Subgroup G) : ↑(Subgroup.op H) = MulOpposite.unop ⁻¹' ↑H

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddSubgroup.mem_op {G : Type u_2} [AddGroup G] {x : Gᵃᵒᵖ} {S : AddSubgroup G} : x ∈ AddSubgroup.op S ↔ AddOpposite.unop x ∈ S

@[simp]

theorem Subgroup.mem_op {G : Type u_2} [Group G] {x : Gᵐᵒᵖ} {S : Subgroup G} : x ∈ Subgroup.op S ↔ MulOpposite.unop x ∈ S

@[simp]

theorem AddSubgroup.op_toAddSubmonoid {G : Type u_2} [AddGroup G] (H : AddSubgroup G) : (AddSubgroup.op H).toAddSubmonoid = AddSubmonoid.op H.toAddSubmonoid

@[simp]

theorem Subgroup.op_toSubmonoid {G : Type u_2} [Group G] (H : Subgroup G) : (Subgroup.op H).toSubmonoid = Submonoid.op H.toSubmonoid

theorem AddSubgroup.unop.proof_3 {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) : ∀ {x : G}, AddOpposite.op x ∈ H → -AddOpposite.op x ∈ H

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

• One or more equations did not get rendered due to their size.

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

theorem AddSubgroup.unop.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) : 0 ∈ H

@[simp]

theorem AddSubgroup.unop_coe {G : Type u_2} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) : ↑(AddSubgroup.unop H) = AddOpposite.op ⁻¹' ↑H

@[simp]

theorem Subgroup.unop_coe {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) : ↑(Subgroup.unop H) = MulOpposite.op ⁻¹' ↑H

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddSubgroup.mem_unop {G : Type u_2} [AddGroup G] {x : G} {S : AddSubgroup Gᵃᵒᵖ} : x ∈ AddSubgroup.unop S ↔ AddOpposite.op x ∈ S

@[simp]

theorem Subgroup.mem_unop {G : Type u_2} [Group G] {x : G} {S : Subgroup Gᵐᵒᵖ} : x ∈ Subgroup.unop S ↔ MulOpposite.op x ∈ S

@[simp]

theorem AddSubgroup.unop_toAddSubmonoid {G : Type u_2} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) : (AddSubgroup.unop H).toAddSubmonoid = AddSubmonoid.unop H.toAddSubmonoid

@[simp]

theorem Subgroup.unop_toSubmonoid {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) : (Subgroup.unop H).toSubmonoid = Submonoid.unop H.toSubmonoid

@[simp]

theorem AddSubgroup.unop_op {G : Type u_2} [AddGroup G] (S : AddSubgroup G) : AddSubgroup.unop (AddSubgroup.op S) = S

@[simp]

theorem Subgroup.unop_op {G : Type u_2} [Group G] (S : Subgroup G) : Subgroup.unop (Subgroup.op S) = S

@[simp]

theorem AddSubgroup.op_unop {G : Type u_2} [AddGroup G] (S : AddSubgroup Gᵃᵒᵖ) : AddSubgroup.op (AddSubgroup.unop S) = S

@[simp]

theorem Subgroup.op_unop {G : Type u_2} [Group G] (S : Subgroup Gᵐᵒᵖ) : Subgroup.op (Subgroup.unop S) = S

Lattice results

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₂

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₂

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₂

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₂

@[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₂

@[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₂

@[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₂

@[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₂

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddSubgroup.opEquiv_apply {G : Type u_2} [AddGroup G] (H : AddSubgroup G) : AddSubgroup.opEquiv H = AddSubgroup.op H

@[simp]

theorem Subgroup.opEquiv_symm_apply {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) : (RelIso.symm Subgroup.opEquiv) H = Subgroup.unop H

@[simp]

theorem Subgroup.opEquiv_apply {G : Type u_2} [Group G] (H : Subgroup G) : Subgroup.opEquiv H = Subgroup.op H

@[simp]

theorem AddSubgroup.opEquiv_symm_apply {G : Type u_2} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) : (RelIso.symm AddSubgroup.opEquiv) H = AddSubgroup.unop H

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

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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₂

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₂

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₂

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₂

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₂

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₂

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₂

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₂

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

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

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

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

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

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

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

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

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)

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)

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)

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)

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)

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)

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)

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)

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

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

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

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

theorem AddSubgroup.equivOp.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ∀ (x : G), x ∈ H ↔ x ∈ H

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

• AddSubgroup.equivOp H = Equiv.subtypeEquiv AddOpposite.opEquiv (_ : ∀ (x : G), x ∈ H ↔ x ∈ H)

@[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

@[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

@[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

@[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

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

• Subgroup.equivOp H = Equiv.subtypeEquiv MulOpposite.opEquiv (_ : ∀ (x : G), x ∈ H ↔ x ∈ H)

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

Equations

• AddSubgroup.instEncodableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupOp H = Encodable.ofEquiv (↥H) (AddSubgroup.equivOp H).symm

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

Equations

• Subgroup.instEncodableSubtypeMulOppositeMemSubgroupGroupInstMembershipInstSetLikeSubgroupOp H = Encodable.ofEquiv (↥H) (Subgroup.equivOp H).symm

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

Equations

• (_ : Countable ↥(AddSubgroup.op H)) = (_ : Countable ↥(AddSubgroup.op H))

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

Equations

• (_ : Countable ↥(Subgroup.op H)) = (_ : Countable ↥(Subgroup.op H))

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)

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