Mathlib.GroupTheory.Subgroup.MulOpposite

source

ink

def AddSubgroup.opposite.proof_2 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) :

∀ {x : Gᵃᵒᵖ}, x.unop ∈ H → -x.unop ∈ H

Equations

(_ : x.unop ∈ H → -x.unop ∈ H) = (_ : x.unop ∈ H → -x.unop ∈ H)

source

ink

def AddSubgroup.opposite.proof_5 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :

∀ {x : G}, { unop := x } ∈ H → -{ unop := x } ∈ H

Equations

(_ : { unop := x } ∈ H → -{ unop := x } ∈ H) = (_ : { unop := x } ∈ H → -{ unop := x } ∈ H)

source

ink

def AddSubgroup.opposite.proof_7 {G : Type u_1} [inst : AddGroup G] :

∀ (x : AddSubgroup Gᵃᵒᵖ), (fun H => { toAddSubmonoid := { toAddSubsemigroup := { carrier := AddOpposite.unop ⁻¹' ↑H, add_mem' := (_ : ∀ {a b : Gᵃᵒᵖ}, a ∈ AddOpposite.unop ⁻¹' ↑H → b ∈ AddOpposite.unop ⁻¹' ↑H → b.unop + a.unop ∈ H) }, zero_mem' := (_ : 0 ∈ H) }, neg_mem' := (_ : ∀ {x : Gᵃᵒᵖ}, x.unop ∈ H → -x.unop ∈ H) }) ((fun H => { toAddSubmonoid := { toAddSubsemigroup := { carrier := AddOpposite.op ⁻¹' ↑H, add_mem' := (_ : ∀ {a b : G}, a ∈ AddOpposite.op ⁻¹' ↑H → b ∈ AddOpposite.op ⁻¹' ↑H → { unop := b } + { unop := a } ∈ H) }, zero_mem' := (_ : 0 ∈ H) }, neg_mem' := (_ : ∀ {x : G}, { unop := x } ∈ H → -{ unop := x } ∈ H) }) x) = x

Equations

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

source

ink

def AddSubgroup.opposite.proof_4 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :

0 ∈ H

Equations

(_ : 0 ∈ H) = (_ : 0 ∈ H)

source

ink

def AddSubgroup.opposite.proof_1 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) :

∀ {a b : Gᵃᵒᵖ}, a ∈ AddOpposite.unop ⁻¹' ↑H → b ∈ AddOpposite.unop ⁻¹' ↑H → b.unop + a.unop ∈ H

Equations

(_ : b.unop + a.unop ∈ H) = (_ : b.unop + a.unop ∈ H)

source

ink

def AddSubgroup.opposite {G : Type u_1} [inst : AddGroup G] :

AddSubgroup G ≃ AddSubgroup Gᵃᵒᵖ

An additive subgroup H of G determines an additive subgroup H.opposite of the opposite additive group Gᵃᵒᵖ.

Equations

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

source

ink

def AddSubgroup.opposite.proof_6 {G : Type u_1} [inst : AddGroup G] :

∀ (x : AddSubgroup G), (fun H => { toAddSubmonoid := { toAddSubsemigroup := { carrier := AddOpposite.op ⁻¹' ↑H, add_mem' := (_ : ∀ {a b : G}, a ∈ AddOpposite.op ⁻¹' ↑H → b ∈ AddOpposite.op ⁻¹' ↑H → { unop := b } + { unop := a } ∈ H) }, zero_mem' := (_ : 0 ∈ H) }, neg_mem' := (_ : ∀ {x : G}, { unop := x } ∈ H → -{ unop := x } ∈ H) }) ((fun H => { toAddSubmonoid := { toAddSubsemigroup := { carrier := AddOpposite.unop ⁻¹' ↑H, add_mem' := (_ : ∀ {a b : Gᵃᵒᵖ}, a ∈ AddOpposite.unop ⁻¹' ↑H → b ∈ AddOpposite.unop ⁻¹' ↑H → b.unop + a.unop ∈ H) }, zero_mem' := (_ : 0 ∈ H) }, neg_mem' := (_ : ∀ {x : Gᵃᵒᵖ}, x.unop ∈ H → -x.unop ∈ H) }) x) = x

Equations

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

source

ink

def AddSubgroup.opposite.proof_3 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :

∀ {a b : G}, a ∈ AddOpposite.op ⁻¹' ↑H → b ∈ AddOpposite.op ⁻¹' ↑H → { unop := b } + { unop := a } ∈ H

Equations

(_ : { unop := b } + { unop := a } ∈ H) = (_ : { unop := b } + { unop := a } ∈ H)

source

ink

def Subgroup.opposite {G : Type u_1} [inst : Group G] :

Subgroup G ≃ Subgroup Gᵐᵒᵖ

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

Equations

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

source

ink

def AddSubgroup.oppositeEquiv.proof_1 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) :

∀ (x : G), x ∈ H ↔ x ∈ H

Equations

(_ : x ∈ H ↔ x ∈ H) = (_ : x ∈ H ↔ x ∈ H)

source

ink

def AddSubgroup.oppositeEquiv {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) :

{ x // x ∈ H } ≃ { x // x ∈ ↑AddSubgroup.opposite H }

Bijection between an additive subgroup H and its opposite.

Equations

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

source

ink

@[simp]

theorem AddSubgroup.oppositeEquiv_apply_coe_unop {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (a : { a // (fun x => x ∈ H) a }) :

(↑(↑(AddSubgroup.oppositeEquiv H) a)).unop = ↑a

source

ink

@[simp]

theorem Subgroup.oppositeEquiv_symm_apply_coe {G : Type u_1} [inst : Group G] (H : Subgroup G) (b : { b // (fun x => x ∈ ↑Subgroup.opposite H) b }) :

↑(↑(Equiv.symm (Subgroup.oppositeEquiv H)) b) = (↑b).unop

source

ink

@[simp]

theorem AddSubgroup.oppositeEquiv_symm_apply_coe {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (b : { b // (fun x => x ∈ ↑AddSubgroup.opposite H) b }) :

↑(↑(Equiv.symm (AddSubgroup.oppositeEquiv H)) b) = (↑b).unop

source

ink

@[simp]

theorem Subgroup.oppositeEquiv_apply_coe_unop {G : Type u_1} [inst : Group G] (H : Subgroup G) (a : { a // (fun x => x ∈ H) a }) :

(↑(↑(Subgroup.oppositeEquiv H) a)).unop = ↑a

source

ink

def Subgroup.oppositeEquiv {G : Type u_1} [inst : Group G] (H : Subgroup G) :

{ x // x ∈ H } ≃ { x // x ∈ ↑Subgroup.opposite H }

Bijection between a subgroup H and its opposite.

Equations

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

source

ink

instance AddSubgroup.instEncodableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupCoeEquivInstFunLikeEquivOpposite {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst : Encodable { x // x ∈ H }] :

Encodable { x // x ∈ ↑AddSubgroup.opposite H }

Equations

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

source

ink

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

Encodable { x // x ∈ ↑Subgroup.opposite H }

Equations

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

source

ink

def AddSubgroup.instCountableSubtypeAddOppositeMemAddSubgroupAddGroupInstMembershipInstSetLikeAddSubgroupCoeEquivInstFunLikeEquivOpposite.proof_1 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst : Countable { x // x ∈ H }] :

Countable { x // x ∈ ↑AddSubgroup.opposite H }

Equations

(_ : Countable { x // x ∈ ↑AddSubgroup.opposite H }) = (_ : Countable { x // x ∈ ↑AddSubgroup.opposite H })

source

ink

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

Countable { x // x ∈ ↑AddSubgroup.opposite H }

Equations

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

source

ink

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

Countable { x // x ∈ ↑Subgroup.opposite H }

Equations

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

source

ink

theorem AddSubgroup.vadd_opposite_add {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} (x : G) (g : G) (h : { x // x ∈ ↑AddSubgroup.opposite H }) :

h +ᵥ (g + x) = g + (h +ᵥ x)

source

ink

theorem Subgroup.smul_opposite_mul {G : Type u_1} [inst : Group G] {H : Subgroup G} (x : G) (g : G) (h : { x // x ∈ ↑Subgroup.opposite H }) :

h • (g * x) = g * h • x

Documentation

Mul-opposite subgroups #

Tags #