Centers of subgroups #

source

def Subgroup.center (G : Type u_1) [Group G] :

Subgroup G

The center of a group G is the set of elements that commute with everything in G

Instances For

source

def AddSubgroup.center (G : Type u_1) [AddGroup G] :

AddSubgroup G

The center of an additive group G is the set of elements that commute with everything in G

Instances For

source

theorem Subgroup.coe_center (G : Type u_1) [Group G] :

↑(center G) = Set.center G

source

theorem AddSubgroup.coe_center (G : Type u_1) [AddGroup G] :

↑(center G) = Set.addCenter G

source

@[simp]

theorem Subgroup.center_toSubmonoid (G : Type u_1) [Group G] :

(center G).toSubmonoid = Submonoid.center G

source

@[simp]

theorem AddSubgroup.center_toAddSubmonoid (G : Type u_1) [AddGroup G] :

(center G).toAddSubmonoid = AddSubmonoid.center G

source

instance Subgroup.center.isMulCommutative (G : Type u_1) [Group G] :

IsMulCommutative ↥(center G)

source

def Subgroup.centerCongr {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) :

↥(center G) ≃* ↥(center H)

The center of isomorphic groups are isomorphic.

Instances For

source

def AddSubgroup.centerCongr {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (e : G ≃+ H) :

↥(center G) ≃+ ↥(center H)

The center of isomorphic additive groups are isomorphic.

Instances For

source

@[simp]

theorem AddSubgroup.centerCongr_apply_coe {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (e : G ≃+ H) (r : ↥(AddSubsemigroup.center G)) :

↑((centerCongr e) r) = e ↑r

source

@[simp]

theorem AddSubgroup.centerCongr_symm_apply_coe {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (e : G ≃+ H) (s : ↥(AddSubsemigroup.center H)) :

↑((centerCongr e).symm s) = e.symm ↑s

source

@[simp]

theorem Subgroup.centerCongr_symm_apply_coe {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) (s : ↥(Subsemigroup.center H)) :

↑((centerCongr e).symm s) = e.symm ↑s

source

@[simp]

theorem Subgroup.centerCongr_apply_coe {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) (r : ↥(Subsemigroup.center G)) :

↑((centerCongr e) r) = e ↑r

source

def Subgroup.centerToMulOpposite (G : Type u_1) [Group G] :

↥(center G) ≃* ↥(center Gᵐᵒᵖ)

The center of a group is isomorphic to the center of its opposite.

Instances For

source

def AddSubgroup.centerToAddOpposite (G : Type u_1) [AddGroup G] :

↥(center G) ≃+ ↥(center Gᵃᵒᵖ)

The center of an additive group is isomorphic to the center of its opposite.

Instances For

source

@[simp]

theorem AddSubgroup.centerToAddOpposite_symm_apply_coe (G : Type u_1) [AddGroup G] (r : ↥(AddSubsemigroup.center Gᵃᵒᵖ)) :

↑((centerToAddOpposite G).symm r) = AddOpposite.unop ↑r

source

@[simp]

theorem AddSubgroup.centerToAddOpposite_apply_coe (G : Type u_1) [AddGroup G] (r : ↥(AddSubsemigroup.center G)) :

↑((centerToAddOpposite G) r) = AddOpposite.op ↑r

source

@[simp]

theorem Subgroup.centerToMulOpposite_apply_coe (G : Type u_1) [Group G] (r : ↥(Subsemigroup.center G)) :

↑((centerToMulOpposite G) r) = MulOpposite.op ↑r

source

@[simp]

theorem Subgroup.centerToMulOpposite_symm_apply_coe (G : Type u_1) [Group G] (r : ↥(Subsemigroup.center Gᵐᵒᵖ)) :

↑((centerToMulOpposite G).symm r) = MulOpposite.unop ↑r

source

theorem Subgroup.mem_center_iff {G : Type u_1} [Group G] {z : G} :

z ∈ center G ↔ ∀ (g : G), g * z = z * g

source

theorem AddSubgroup.mem_center_iff {G : Type u_1} [AddGroup G] {z : G} :

z ∈ center G ↔ ∀ (g : G), g + z = z + g

source

@[instance_reducible]

instance Subgroup.decidableMemCenter {G : Type u_1} [Group G] (z : G) [Decidable (∀ (g : G), g * z = z * g)] :

Decidable (z ∈ center G)

source

theorem Subgroup.map_center_le_center {G : Type u_1} {H : Type u_2} [Group G] [Group H] {F : Type u_3} [FunLike F G H] [MonoidHomClass F G H] {f : F} (hf : Function.Surjective ⇑f) :

map (↑f) (center G) ≤ center H

source

theorem AddSubgroup.map_center_le_center {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {F : Type u_3} [FunLike F G H] [AddMonoidHomClass F G H] {f : F} (hf : Function.Surjective ⇑f) :

map (↑f) (center G) ≤ center H

source

theorem Subgroup.comap_center_le_center {G : Type u_1} {H : Type u_2} [Group G] [Group H] {F : Type u_3} [FunLike F G H] [MonoidHomClass F G H] {f : F} (hf : Function.Injective ⇑f) :

comap (↑f) (center H) ≤ center G

source

theorem AddSubgroup.comap_center_le_center {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {F : Type u_3} [FunLike F G H] [AddMonoidHomClass F G H] {f : F} (hf : Function.Injective ⇑f) :

comap (↑f) (center H) ≤ center G

source

@[simp]

theorem Subgroup.map_center_eq {G : Type u_1} {H : Type u_2} [Group G] [Group H] {F : Type u_3} [EquivLike F G H] [MulEquivClass F G H] (f : F) :

map (↑f) (center G) = center H

source

@[simp]

theorem AddSubgroup.map_center_eq {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {F : Type u_3} [EquivLike F G H] [AddEquivClass F G H] (f : F) :

map (↑f) (center G) = center H

source

instance Subgroup.centerCharacteristic {G : Type u_1} [Group G] :

(center G).Characteristic

source

instance AddSubgroup.centerCharacteristic {G : Type u_1} [AddGroup G] :

(center G).Characteristic

source

theorem CommGroup.center_eq_top {G : Type u_3} [CommGroup G] :

Subgroup.center G = ⊤

source

theorem AddCommGroup.center_eq_top {G : Type u_3} [AddCommGroup G] :

AddSubgroup.center G = ⊤

source

theorem Subgroup.center_eq_top_iff {G : Type u_1} [Group G] :

center G = ⊤ ↔ IsMulCommutative G

source

theorem AddSubgroup.center_eq_top_iff {G : Type u_1} [AddGroup G] :

center G = ⊤ ↔ IsAddCommutative G

source

theorem Subgroup.center_eq_top {G : Type u_1} [Group G] [hG : IsMulCommutative G] :

center G = ⊤

source

theorem AddSubgroup.center_eq_top {G : Type u_1} [AddGroup G] [hG : IsAddCommutative G] :

center G = ⊤

source

@[instance_reducible]

def Group.commGroupOfCenterEqTop {G : Type u_1} [Group G] (h : Subgroup.center G = ⊤) :

CommGroup G

A group is commutative if the center is the whole group.

Instances For

source

def AddGroup.addCommGroupOfCenterEqTop {G : Type u_1} [AddGroup G] (h : AddSubgroup.center G = ⊤) :

AddCommGroup G

An additive group is commutative if the center is the whole group.

Instances For

source

theorem Subgroup.center_prod {G : Type u_1} {H : Type u_2} [Group G] [Group H] :

center (G × H) = (center G).prod (center H)

source

theorem AddSubgroup.center_sum {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] :

center (G × H) = (center G).prod (center H)

source

theorem Subgroup.center_pi {η : Type u_3} {G : η → Type u_4} [(i : η) → Group (G i)] :

center ((i : η) → G i) = pi Set.univ fun (i : η) => center (G i)

source

theorem AddSubgroup.center_pi {η : Type u_3} {G : η → Type u_4} [(i : η) → AddGroup (G i)] :

center ((i : η) → G i) = pi Set.univ fun (i : η) => center (G i)

source

theorem Subgroup.normal_of_le_center {G : Type u_1} [Group G] {H : Subgroup G} (hH : H ≤ center G) :

H.Normal

source

theorem AddSubgroup.normal_of_le_center {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hH : H ≤ center G) :

H.Normal

source

instance Subgroup.instNormalCenter {G : Type u_1} [Group G] :

(center G).Normal

source

instance AddSubgroup.instNormalCenter {G : Type u_1} [AddGroup G] :

(center G).Normal

source

theorem Subgroup.center_le_normalizer {G : Type u_1} [Group G] (s : Set G) :

center G ≤ normalizer s

source

theorem AddSubgroup.center_le_normalizer {G : Type u_1} [AddGroup G] (s : Set G) :

center G ≤ normalizer s

source

theorem IsConj.eq_of_left_mem_center {M : Type u_3} [Monoid M] {g h : M} (H : IsConj g h) (Hg : g ∈ Set.center M) :

g = h

source

theorem IsConj.eq_of_right_mem_center {M : Type u_3} [Monoid M] {g h : M} (H : IsConj g h) (Hh : h ∈ Set.center M) :

g = h

source

theorem ConjClasses.mk_bijOn (G : Type u_3) [Group G] :

Set.BijOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Documentation

Mathlib.GroupTheory.Subgroup.Center

Centers of subgroups #