Mul-opposite subgroups

Tags

subgroup, subgroups

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

Equations

• H.op = { carrier := MulOpposite.unop ⁻¹' ↑H, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

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

Equations

• H.op = { carrier := AddOpposite.unop ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Subgroup.op_toSubsemigroup {G : Type u_1} [Group G] (H : Subgroup G) : H.op.toSubsemigroup = H.op

theorem AddSubgroup.op_toSubsemigroup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.op.toAddSubsemigroup = H.op

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

Equations

• H.unop = { carrier := MulOpposite.op ⁻¹' ↑H, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

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

Equations

• H.unop = { carrier := AddOpposite.op ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Subgroup.unop_toSubsemigroup {G : Type u_1} [Group G] (H : Subgroup Gᵐᵒᵖ) : H.unop.toSubsemigroup = H.unop

theorem AddSubgroup.unop_toSubsemigroup {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) : H.unop.toAddSubsemigroup = H.unop

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Lattice results

theorem Subgroup.op_le_iff {G : Type u_1} [Group G] {S₁ : Subgroup G} {S₂ : Subgroup Gᵐᵒᵖ} : S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop

theorem AddSubgroup.op_le_iff {G : Type u_1} [AddGroup G] {S₁ : AddSubgroup G} {S₂ : AddSubgroup Gᵃᵒᵖ} : S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop

theorem Subgroup.le_op_iff {G : Type u_1} [Group G] {S₁ : Subgroup Gᵐᵒᵖ} {S₂ : Subgroup G} : S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂

theorem AddSubgroup.le_op_iff {G : Type u_1} [AddGroup G] {S₁ : AddSubgroup Gᵃᵒᵖ} {S₂ : AddSubgroup G} : S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂

@[simp]

theorem Subgroup.op_le_op_iff {G : Type u_1} [Group G] {S₁ S₂ : Subgroup G} : S₁.op ≤ S₂.op ↔ S₁ ≤ S₂

@[simp]

theorem AddSubgroup.op_le_op_iff {G : Type u_1} [AddGroup G] {S₁ S₂ : AddSubgroup G} : S₁.op ≤ S₂.op ↔ S₁ ≤ S₂

@[simp]

theorem Subgroup.unop_le_unop_iff {G : Type u_1} [Group G] {S₁ S₂ : Subgroup Gᵐᵒᵖ} : S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂

@[simp]

theorem AddSubgroup.unop_le_unop_iff {G : Type u_1} [AddGroup G] {S₁ S₂ : AddSubgroup Gᵃᵒᵖ} : S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂

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ᵐᵒᵖ.

Equations

• Subgroup.opEquiv = { toFun := Subgroup.op, invFun := Subgroup.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

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ᵃᵒᵖ.

Equations

• AddSubgroup.opEquiv = { toFun := AddSubgroup.op, invFun := AddSubgroup.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Subgroup.op_injective {G : Type u_1} [Group G] : Function.Injective Subgroup.op

theorem AddSubgroup.op_injective {G : Type u_1} [AddGroup G] : Function.Injective AddSubgroup.op

theorem Subgroup.unop_injective {G : Type u_1} [Group G] : Function.Injective Subgroup.unop

theorem AddSubgroup.unop_injective {G : Type u_1} [AddGroup G] : Function.Injective AddSubgroup.unop

@[simp]

theorem Subgroup.op_inj {G : Type u_1} [Group G] {S T : Subgroup G} : S.op = T.op ↔ S = T

@[simp]

theorem AddSubgroup.op_inj {G : Type u_1} [AddGroup G] {S T : AddSubgroup G} : S.op = T.op ↔ S = T

@[simp]

theorem Subgroup.unop_inj {G : Type u_1} [Group G] {S T : Subgroup Gᵐᵒᵖ} : S.unop = T.unop ↔ S = T

@[simp]

theorem AddSubgroup.unop_inj {G : Type u_1} [AddGroup G] {S T : AddSubgroup Gᵃᵒᵖ} : S.unop = T.unop ↔ S = T

def Subgroup.equivOp {G : Type u_1} [Group G] (H : Subgroup G) : ↥H ≃ ↥H.op

Bijection between a subgroup H and its opposite.

Equations

• H.equivOp = MulOpposite.opEquiv.subtypeEquiv ⋯

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

Bijection between an additive subgroup H and its opposite.

Equations

• H.equivOp = AddOpposite.opEquiv.subtypeEquiv ⋯

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

@[simp]

theorem AddSubgroup.equivOp_apply_coe {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (a : ↥H) : ↑(H.equivOp a) = AddOpposite.op ↑a

@[simp]

theorem Subgroup.equivOp_apply_coe {G : Type u_1} [Group G] (H : Subgroup G) (a : ↥H) : ↑(H.equivOp a) = MulOpposite.op ↑a

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

theorem Subgroup.op_normalizer {G : Type u_1} [Group G] (H : Subgroup G) : (normalizer ↑H).op = normalizer ↑H.op

theorem AddSubgroup.op_normalizer {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : (normalizer ↑H).op = normalizer ↑H.op

theorem Subgroup.unop_normalizer {G : Type u_1} [Group G] (H : Subgroup Gᵐᵒᵖ) : (normalizer ↑H).unop = normalizer ↑H.unop

theorem AddSubgroup.unop_normalizer {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) : (normalizer ↑H).unop = normalizer ↑H.unop

def Subgroup.mulEquivOpMop {G : Type u_1} [Group G] (S : Subgroup G) : ↥S ≃* (↥S.op)ᵐᵒᵖ

Bijection between a subgroup S and MulOpposite of its opposite.

Equations

• S.mulEquivOpMop = { toEquiv := S.equivOp.trans MulOpposite.opEquiv, map_mul' := ⋯ }

@[simp]

theorem AddSubgroup.addEquivOpAop_symm_apply_coe {G : Type u_1} [AddGroup G] (S : AddSubgroup G) (a✝ : (↥S.op)ᵃᵒᵖ) : ↑(S.addEquivOpAop.symm a✝) = AddOpposite.unop ↑(AddOpposite.unop a✝)

@[simp]

theorem AddSubgroup.addEquivOpAop_apply {G : Type u_1} [AddGroup G] (S : AddSubgroup G) (a✝ : ↥S) : S.addEquivOpAop a✝ = AddOpposite.op (S.equivOp a✝)

@[simp]

theorem Subgroup.mulEquivOpMop_apply {G : Type u_1} [Group G] (S : Subgroup G) (a✝ : ↥S) : S.mulEquivOpMop a✝ = MulOpposite.op (S.equivOp a✝)

@[simp]

theorem Subgroup.mulEquivOpMop_symm_apply_coe {G : Type u_1} [Group G] (S : Subgroup G) (a✝ : (↥S.op)ᵐᵒᵖ) : ↑(S.mulEquivOpMop.symm a✝) = MulOpposite.unop ↑(MulOpposite.unop a✝)

def AddSubgroup.addEquivOpAop {G : Type u_1} [AddGroup G] (S : AddSubgroup G) : ↥S ≃+ (↥S.op)ᵃᵒᵖ

Bijection between an additive subgroup and AddOpposite of its opposite.

Equations

• S.addEquivOpAop = { toEquiv := S.equivOp.trans AddOpposite.opEquiv, map_add' := ⋯ }

def Subgroup.mopMulEquivOp {G : Type u_1} [Group G] (S : Subgroup G) : (↥S)ᵐᵒᵖ ≃* ↥S.op

Bijection between MulOpposite of a subgroup S and its opposite.

Equations

• S.mopMulEquivOp = { toEquiv := MulOpposite.opEquiv.symm.trans S.equivOp, map_mul' := ⋯ }

@[simp]

theorem Subgroup.mopMulEquivOp_apply_coe {G : Type u_1} [Group G] (S : Subgroup G) (a✝ : (↥S)ᵐᵒᵖ) : ↑(S.mopMulEquivOp a✝) = MulOpposite.op ↑(MulOpposite.unop a✝)

@[simp]

theorem Subgroup.mopMulEquivOp_symm_apply {G : Type u_1} [Group G] (S : Subgroup G) (a✝ : ↥S.op) : S.mopMulEquivOp.symm a✝ = MulOpposite.op (S.equivOp.symm a✝)

@[simp]

theorem AddSubgroup.aopAddEquivOp_symm_apply {G : Type u_1} [AddGroup G] (S : AddSubgroup G) (a✝ : ↥S.op) : S.aopAddEquivOp.symm a✝ = AddOpposite.op (S.equivOp.symm a✝)

@[simp]

theorem AddSubgroup.aopAddEquivOp_apply_coe {G : Type u_1} [AddGroup G] (S : AddSubgroup G) (a✝ : (↥S)ᵃᵒᵖ) : ↑(S.aopAddEquivOp a✝) = AddOpposite.op ↑(AddOpposite.unop a✝)

def AddSubgroup.aopAddEquivOp {G : Type u_1} [AddGroup G] (S : AddSubgroup G) : (↥S)ᵃᵒᵖ ≃+ ↥S.op

Bijection between AddOpposite of an additive subgroup and its opposite.

Equations

• S.aopAddEquivOp = { toEquiv := AddOpposite.opEquiv.symm.trans S.equivOp, map_add' := ⋯ }

def Subgroup.mulEquivOp {G : Type u_1} [CommGroup G] (S : Subgroup G) : ↥S ≃* ↥S.op

Bijection between a subgroup S and its opposite as a monoid equivalence.

Equations

• S.mulEquivOp = { toEquiv := S.equivOp, map_mul' := ⋯ }

def AddSubgroup.addEquivOp {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) : ↥S ≃+ ↥S.op

Bijection between an additive subgroup and its opposite as an additive equivalence.

Equations

• S.addEquivOp = { toEquiv := S.equivOp, map_add' := ⋯ }

@[simp]

theorem Subgroup.mulEquivOp_symm_apply_coe {G : Type u_1} [CommGroup G] (S : Subgroup G) (b : ↥S.op) : ↑(S.mulEquivOp.symm b) = MulOpposite.unop ↑b

@[simp]

theorem Subgroup.mulEquivOp_apply_coe {G : Type u_1} [CommGroup G] (S : Subgroup G) (a : ↥S) : ↑(S.mulEquivOp a) = MulOpposite.op ↑a

@[simp]

theorem AddSubgroup.addEquivOp_apply_coe {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (a : ↥S) : ↑(S.addEquivOp a) = AddOpposite.op ↑a

@[simp]

theorem AddSubgroup.addEquivOp_symm_apply_coe {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (b : ↥S.op) : ↑(S.addEquivOp.symm b) = AddOpposite.unop ↑b