Centers of subgroups

theorem AddSubgroup.center.proof_2 (G : Type u_1) [AddGroup G] : 0 ∈ (AddSubmonoid.center G).carrier

theorem AddSubgroup.center.proof_1 (G : Type u_1) [AddGroup G] : ∀ {a b : G}, a ∈ (AddSubmonoid.center G).carrier → b ∈ (AddSubmonoid.center G).carrier → a + b ∈ (AddSubmonoid.center G).carrier

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

Equations

• AddSubgroup.center G = let __src := AddSubmonoid.center G; { toAddSubmonoid := { toAddSubsemigroup := { carrier := Set.addCenter G, add_mem' := ⋯ }, zero_mem' := ⋯ }, neg_mem' := ⋯ }

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

Equations

• Subgroup.center G = let __src := Submonoid.center G; { toSubmonoid := { toSubsemigroup := { carrier := Set.center G, mul_mem' := ⋯ }, one_mem' := ⋯ }, inv_mem' := ⋯ }

theorem AddSubgroup.coe_center (G : Type u_1) [AddGroup G] : ↑(AddSubgroup.center G) = Set.addCenter G

theorem Subgroup.coe_center (G : Type u_1) [Group G] : ↑(Subgroup.center G) = Set.center G

@[simp]

theorem AddSubgroup.center_toAddSubmonoid (G : Type u_1) [AddGroup G] : (AddSubgroup.center G).toAddSubmonoid = AddSubmonoid.center G

@[simp]

theorem Subgroup.center_toSubmonoid (G : Type u_1) [Group G] : (Subgroup.center G).toSubmonoid = Submonoid.center G

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

Equations

• ⋯ = ⋯

@[simp]

theorem Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe (G₀ : Type u_2) [GroupWithZero G₀] (u : (↥(Submonoid.center G₀))ˣ) : ↑↑((MulEquiv.symm (Subgroup.centerUnitsEquivUnitsCenter G₀)) u) = ↑↑u

@[simp]

theorem Subgroup.val_centerUnitsEquivUnitsCenter_apply_coe (G₀ : Type u_2) [GroupWithZero G₀] (a : ↥(Subgroup.center G₀ˣ)) : ↑↑((Subgroup.centerUnitsEquivUnitsCenter G₀) a) = ↑↑a

def Subgroup.centerUnitsEquivUnitsCenter (G₀ : Type u_2) [GroupWithZero G₀] : ↥(Subgroup.center G₀ˣ) ≃* (↥(Submonoid.center G₀))ˣ

For a group with zero, the center of the units is the same as the units of the center.

Equations

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

theorem AddSubgroup.mem_center_iff {G : Type u_1} [AddGroup G] {z : G} : z ∈ AddSubgroup.center G ↔ ∀ (g : G), g + z = z + g

theorem Subgroup.mem_center_iff {G : Type u_1} [Group G] {z : G} : z ∈ Subgroup.center G ↔ ∀ (g : G), g * z = z * g

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

Equations

• Subgroup.decidableMemCenter z = decidable_of_iff' (∀ (g : G), g * z = z * g) ⋯

instance AddSubgroup.centerCharacteristic {G : Type u_1} [AddGroup G] : AddSubgroup.Characteristic (AddSubgroup.center G)

Equations

• ⋯ = ⋯

instance Subgroup.centerCharacteristic {G : Type u_1} [Group G] : Subgroup.Characteristic (Subgroup.center G)

Equations

• ⋯ = ⋯

theorem CommGroup.center_eq_top {G : Type u_2} [CommGroup G] : Subgroup.center G = ⊤

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

Equations

• Group.commGroupOfCenterEqTop h = let __src := inst; CommGroup.mk ⋯

theorem AddSubgroup.center_le_normalizer {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : AddSubgroup.center G ≤ AddSubgroup.normalizer H

theorem Subgroup.center_le_normalizer {G : Type u_1} [Group G] {H : Subgroup G} : Subgroup.center G ≤ Subgroup.normalizer H

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

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

theorem ConjClasses.mk_bijOn (G : Type u_2) [Group G] : Set.BijOn ConjClasses.mk (↑(Subgroup.center G)) (ConjClasses.noncenter G)ᶜ