Documentation

Mathlib.GroupTheory.Subgroup.MulOpposite

Mul-opposite subgroups #

Tags #

subgroup, subgroups

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)
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)
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 ⁻¹' Hb AddOpposite.unop ⁻¹' Hb.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 ⁻¹' Hb 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.
def AddSubgroup.opposite.proof_4 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
0 H
Equations
def AddSubgroup.opposite.proof_1 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) :
∀ {a b : Gᵃᵒᵖ}, a AddOpposite.unop ⁻¹' Hb AddOpposite.unop ⁻¹' Hb.unop + a.unop H
Equations
  • (_ : b.unop + a.unop H) = (_ : b.unop + a.unop H)

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.
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 ⁻¹' Hb 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 ⁻¹' Hb AddOpposite.unop ⁻¹' Hb.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.
def AddSubgroup.opposite.proof_3 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
∀ {a b : G}, a AddOpposite.op ⁻¹' Hb AddOpposite.op ⁻¹' H{ unop := b } + { unop := a } H
Equations
  • (_ : { unop := b } + { unop := a } H) = (_ : { unop := b } + { unop := a } H)

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.
def AddSubgroup.oppositeEquiv.proof_1 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) :
∀ (x : G), x H x H
Equations
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
@[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
@[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
@[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
@[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
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
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
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)
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