Mul-opposite subgroups

Tags

subgroup, subgroups

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

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

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

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

@[simp]

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

@[simp]

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

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

• 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_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_1} [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_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) : 0 ∈ H

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem AddSubgroup.opEquiv.proof_2 {G : Type u_1} [AddGroup G] : ∀ (x : AddSubgroup Gᵃᵒᵖ), AddSubgroup.op (AddSubgroup.unop x) = x

def AddSubgroup.opEquiv {G : Type u_1} [AddGroup G] : AddSubgroup G ≃ 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.

theorem AddSubgroup.opEquiv.proof_1 {G : Type u_1} [AddGroup G] : ∀ (x : AddSubgroup G), AddSubgroup.unop (AddSubgroup.op x) = x

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def Subgroup.opEquiv {G : Type u_1} [Group G] : Subgroup G ≃ 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.

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_1} [AddGroup G] (H : AddSubgroup G) : { x // x ∈ H } ≃ { x // x ∈ 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 AddSubgroup.equivOp_apply_coe {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (a : { a // (fun x => x ∈ H) a }) : ↑(↑(AddSubgroup.equivOp H) a) = AddOpposite.op ↑a

@[simp]

theorem Subgroup.equivOp_symm_apply_coe {G : Type u_1} [Group G] (H : Subgroup G) (b : { b // (fun x => x ∈ Subgroup.op H) b }) : ↑(↑(Subgroup.equivOp H).symm b) = MulOpposite.unop ↑b

@[simp]

theorem AddSubgroup.equivOp_symm_apply_coe {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (b : { b // (fun x => x ∈ AddSubgroup.op H) b }) : ↑(↑(AddSubgroup.equivOp H).symm b) = AddOpposite.unop ↑b

@[simp]

theorem Subgroup.equivOp_apply_coe {G : Type u_1} [Group G] (H : Subgroup G) (a : { a // (fun x => x ∈ H) a }) : ↑(↑(Subgroup.equivOp H) a) = MulOpposite.op ↑a

def Subgroup.equivOp {G : Type u_1} [Group G] (H : Subgroup G) : { x // x ∈ H } ≃ { x // x ∈ 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_1} [AddGroup G] (H : AddSubgroup G) [Encodable { x // x ∈ H }] : Encodable { x // x ∈ AddSubgroup.op H }

Equations

• AddSubgroup.instEncodableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupOp H = Encodable.ofEquiv { x // x ∈ H } (AddSubgroup.equivOp H).symm

instance Subgroup.instEncodableSubtypeMulOppositeMemSubgroupGroupInstMembershipInstSetLikeSubgroupOp {G : Type u_1} [Group G] (H : Subgroup G) [Encodable { x // x ∈ H }] : Encodable { x // x ∈ Subgroup.op H }

Equations

• Subgroup.instEncodableSubtypeMulOppositeMemSubgroupGroupInstMembershipInstSetLikeSubgroupOp H = Encodable.ofEquiv { x // x ∈ H } (Subgroup.equivOp H).symm

instance AddSubgroup.instCountableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupOp {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Countable { x // x ∈ H }] : Countable { x // x ∈ AddSubgroup.op H }

Equations

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

theorem AddSubgroup.instCountableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupOp.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Countable { x // x ∈ H }] : Countable { x // x ∈ AddSubgroup.op H }

instance Subgroup.instCountableSubtypeMulOppositeMemSubgroupGroupInstMembershipInstSetLikeSubgroupOp {G : Type u_1} [Group G] (H : Subgroup G) [Countable { x // x ∈ H }] : Countable { x // x ∈ Subgroup.op H }

Equations

• @Subgroup.instCountableSubtypeMulOppositeMemSubgroupGroupInstMembershipInstSetLikeSubgroupOp = @Subgroup.instCountableSubtypeMulOppositeMemSubgroupGroupInstMembershipInstSetLikeSubgroupOp.proof_1

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

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