Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
refactor(group_theory/{submonoid, subsemigroup}/{center, centralizer}…
…): move set.center and set.centralizer into subsemigroup (#13903) This moves `set.center` and `set.centralizer` (the center and centralizers for a magma) into `group_theory/subsemigroup/{center, centralizer}` so that we can define the center and centralizers for semigroups in #13627.
- Loading branch information
Showing
4 changed files
with
231 additions
and
194 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,114 @@ | ||
| /- | ||
| Copyright (c) 2021 Eric Wieser. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Eric Wieser, Jireh Loreaux | ||
| -/ | ||
| import group_theory.subsemigroup.operations | ||
| import data.fintype.basic | ||
|
|
||
| /-! | ||
| # Centers of magmas and semigroups | ||
| ## Main definitions | ||
| * `set.center`: the center of a magma | ||
| * `set.add_center`: the center of an additive magma | ||
| We provide `submonoid.center`, `add_submonoid.center`, `subgroup.center`, `add_subgroup.center`, | ||
| `subsemiring.center`, and `subring.center` in other files. | ||
| -/ | ||
|
|
||
| variables {M : Type*} | ||
|
|
||
| namespace set | ||
|
|
||
| variables (M) | ||
|
|
||
| /-- The center of a magma. -/ | ||
| @[to_additive add_center /-" The center of an additive magma. "-/] | ||
| def center [has_mul M] : set M := {z | ∀ m, m * z = z * m} | ||
|
|
||
| @[to_additive mem_add_center] | ||
| lemma mem_center_iff [has_mul M] {z : M} : z ∈ center M ↔ ∀ g, g * z = z * g := iff.rfl | ||
|
|
||
| instance decidable_mem_center [has_mul M] [decidable_eq M] [fintype M] : | ||
| decidable_pred (∈ center M) := | ||
| λ _, decidable_of_iff' _ (mem_center_iff M) | ||
|
|
||
| @[simp, to_additive zero_mem_add_center] | ||
| lemma one_mem_center [mul_one_class M] : (1 : M) ∈ set.center M := by simp [mem_center_iff] | ||
|
|
||
| @[simp] | ||
| lemma zero_mem_center [mul_zero_class M] : (0 : M) ∈ set.center M := by simp [mem_center_iff] | ||
|
|
||
| variables {M} | ||
|
|
||
| @[simp, to_additive add_mem_add_center] | ||
| lemma mul_mem_center [semigroup M] {a b : M} | ||
| (ha : a ∈ set.center M) (hb : b ∈ set.center M) : a * b ∈ set.center M := | ||
| λ g, by rw [mul_assoc, ←hb g, ← mul_assoc, ha g, mul_assoc] | ||
|
|
||
| @[simp, to_additive neg_mem_add_center] | ||
| lemma inv_mem_center [group M] {a : M} (ha : a ∈ set.center M) : a⁻¹ ∈ set.center M := | ||
| λ g, by rw [← inv_inj, mul_inv_rev, inv_inv, ← ha, mul_inv_rev, inv_inv] | ||
|
|
||
| @[simp] | ||
| lemma add_mem_center [distrib M] {a b : M} | ||
| (ha : a ∈ set.center M) (hb : b ∈ set.center M) : a + b ∈ set.center M := | ||
| λ c, by rw [add_mul, mul_add, ha c, hb c] | ||
|
|
||
| @[simp] | ||
| lemma neg_mem_center [ring M] {a : M} (ha : a ∈ set.center M) : -a ∈ set.center M := | ||
| λ c, by rw [←neg_mul_comm, ha (-c), neg_mul_comm] | ||
|
|
||
| @[to_additive subset_add_center_add_units] | ||
| lemma subset_center_units [monoid M] : | ||
| (coe : Mˣ → M) ⁻¹' center M ⊆ set.center Mˣ := | ||
| λ a ha b, units.ext $ ha _ | ||
|
|
||
| lemma center_units_subset [group_with_zero M] : | ||
| set.center Mˣ ⊆ (coe : Mˣ → M) ⁻¹' center M := | ||
| λ a ha b, begin | ||
| obtain rfl | hb := eq_or_ne b 0, | ||
| { rw [zero_mul, mul_zero], }, | ||
| { exact units.ext_iff.mp (ha (units.mk0 _ hb)) } | ||
| end | ||
|
|
||
| /-- In a group with zero, the center of the units is the preimage of the center. -/ | ||
| lemma center_units_eq [group_with_zero M] : | ||
| set.center Mˣ = (coe : Mˣ → M) ⁻¹' center M := | ||
| subset.antisymm center_units_subset subset_center_units | ||
|
|
||
| @[simp] | ||
| lemma inv_mem_center₀ [group_with_zero M] {a : M} (ha : a ∈ set.center M) : a⁻¹ ∈ set.center M := | ||
| begin | ||
| obtain rfl | ha0 := eq_or_ne a 0, | ||
| { rw inv_zero, exact zero_mem_center M }, | ||
| rcases is_unit.mk0 _ ha0 with ⟨a, rfl⟩, | ||
| rw ←units.coe_inv', | ||
| exact center_units_subset (inv_mem_center (subset_center_units ha)), | ||
| end | ||
|
|
||
| @[simp, to_additive sub_mem_add_center] | ||
| lemma div_mem_center [group M] {a b : M} (ha : a ∈ set.center M) (hb : b ∈ set.center M) : | ||
| a / b ∈ set.center M := | ||
| begin | ||
| rw [div_eq_mul_inv], | ||
| exact mul_mem_center ha (inv_mem_center hb), | ||
| end | ||
|
|
||
| @[simp] | ||
| lemma div_mem_center₀ [group_with_zero M] {a b : M} (ha : a ∈ set.center M) | ||
| (hb : b ∈ set.center M) : a / b ∈ set.center M := | ||
| begin | ||
| rw div_eq_mul_inv, | ||
| exact mul_mem_center ha (inv_mem_center₀ hb), | ||
| end | ||
|
|
||
| variables (M) | ||
|
|
||
| @[simp, to_additive add_center_eq_univ] | ||
| lemma center_eq_univ [comm_semigroup M] : center M = set.univ := | ||
| subset.antisymm (subset_univ _) $ λ x _ y, mul_comm y x | ||
|
|
||
| end set |
Oops, something went wrong.