Centers of subgroups #
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
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' := ⋯ }
Instances For
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' := ⋯ }
Instances For
theorem
AddSubgroup.coe_center
(G : Type u_1)
[AddGroup G]
:
↑(AddSubgroup.center G) = Set.addCenter 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
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.
Instances For
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) ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A group is commutative if the center is the whole group
Equations
- Group.commGroupOfCenterEqTop h = let __src := inst; CommGroup.mk ⋯
Instances For
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)ᶜ