diff --git a/src/algebra/periodic.lean b/src/algebra/periodic.lean index 442c4cafb585b..9404f8a061254 100644 --- a/src/algebra/periodic.lean +++ b/src/algebra/periodic.lean @@ -8,6 +8,7 @@ import algebra.module.basic import algebra.order.archimedean import data.int.parity import group_theory.coset +import group_theory.subgroup.zpowers /-! # Periodicity diff --git a/src/group_theory/coset.lean b/src/group_theory/coset.lean index 48d24dd1d9afa..2eee06e3571d5 100644 --- a/src/group_theory/coset.lean +++ b/src/group_theory/coset.lean @@ -6,6 +6,7 @@ Authors: Mitchell Rowett, Scott Morrison import algebra.quotient import group_theory.group_action.basic +import group_theory.subgroup.mul_opposite import tactic.group /-! diff --git a/src/group_theory/group_action/conj_act.lean b/src/group_theory/group_action/conj_act.lean index 6c216817766fe..5a9ed7a2ffb8c 100644 --- a/src/group_theory/group_action/conj_act.lean +++ b/src/group_theory/group_action/conj_act.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes -/ import group_theory.group_action.basic -import group_theory.subgroup.basic +import group_theory.subgroup.zpowers import algebra.group_ring_action.basic /-! # Conjugation action of a group on itself diff --git a/src/group_theory/group_action/fixing_subgroup.lean b/src/group_theory/group_action/fixing_subgroup.lean index 3718d4c8ac4da..ba7d078189e48 100644 --- a/src/group_theory/group_action/fixing_subgroup.lean +++ b/src/group_theory/group_action/fixing_subgroup.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Antoine Chambert-Loir -/ -import group_theory.subgroup.basic +import group_theory.subgroup.actions import group_theory.group_action.basic /-! diff --git a/src/group_theory/solvable.lean b/src/group_theory/solvable.lean index e9ae039668dda..d02f872a54c4d 100644 --- a/src/group_theory/solvable.lean +++ b/src/group_theory/solvable.lean @@ -7,6 +7,7 @@ Authors: Jordan Brown, Thomas Browning, Patrick Lutz import data.fin.vec_notation import group_theory.abelianization import group_theory.perm.via_embedding +import group_theory.subgroup.simple import set_theory.cardinal.basic /-! diff --git a/src/group_theory/specific_groups/alternating.lean b/src/group_theory/specific_groups/alternating.lean index 5fddc8b655f95..5f4a13d2e7245 100644 --- a/src/group_theory/specific_groups/alternating.lean +++ b/src/group_theory/specific_groups/alternating.lean @@ -6,6 +6,7 @@ Authors: Aaron Anderson import algebra.group.conj_finite import group_theory.perm.fin +import group_theory.subgroup.simple import tactic.interval_cases /-! diff --git a/src/group_theory/specific_groups/cyclic.lean b/src/group_theory/specific_groups/cyclic.lean index 21e961156bfdb..9a48297f65a54 100644 --- a/src/group_theory/specific_groups/cyclic.lean +++ b/src/group_theory/specific_groups/cyclic.lean @@ -7,6 +7,7 @@ Authors: Johannes Hölzl import algebra.big_operators.order import data.nat.totient import group_theory.order_of_element +import group_theory.subgroup.simple import tactic.group import group_theory.exponent diff --git a/src/group_theory/subgroup/actions.lean b/src/group_theory/subgroup/actions.lean new file mode 100644 index 0000000000000..c3d8d0ad3fa79 --- /dev/null +++ b/src/group_theory/subgroup/actions.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2021 Eric Wieser. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Eric Wieser +-/ + +import group_theory.subgroup.basic + +/-! +# Actions by `subgroup`s + +These are just copies of the definitions about `submonoid` starting from `submonoid.mul_action`. + +## Tags +subgroup, subgroups + +-/ + +namespace subgroup + +variables {G : Type*} [group G] +variables {α β : Type*} + +/-- The action by a subgroup is the action by the underlying group. -/ +@[to_additive /-"The additive action by an add_subgroup is the action by the underlying +add_group. "-/] +instance [mul_action G α] (S : subgroup G) : mul_action S α := +S.to_submonoid.mul_action + +@[to_additive] +lemma smul_def [mul_action G α] {S : subgroup G} (g : S) (m : α) : g • m = (g : G) • m := rfl + +@[to_additive] +instance smul_comm_class_left + [mul_action G β] [has_smul α β] [smul_comm_class G α β] (S : subgroup G) : + smul_comm_class S α β := +S.to_submonoid.smul_comm_class_left + +@[to_additive] +instance smul_comm_class_right + [has_smul α β] [mul_action G β] [smul_comm_class α G β] (S : subgroup G) : + smul_comm_class α S β := +S.to_submonoid.smul_comm_class_right + +/-- Note that this provides `is_scalar_tower S G G` which is needed by `smul_mul_assoc`. -/ +instance + [has_smul α β] [mul_action G α] [mul_action G β] [is_scalar_tower G α β] (S : subgroup G) : + is_scalar_tower S α β := +S.to_submonoid.is_scalar_tower + +instance [mul_action G α] [has_faithful_smul G α] (S : subgroup G) : + has_faithful_smul S α := +S.to_submonoid.has_faithful_smul + +/-- The action by a subgroup is the action by the underlying group. -/ +instance [add_monoid α] [distrib_mul_action G α] (S : subgroup G) : distrib_mul_action S α := +S.to_submonoid.distrib_mul_action + +/-- The action by a subgroup is the action by the underlying group. -/ +instance [monoid α] [mul_distrib_mul_action G α] (S : subgroup G) : mul_distrib_mul_action S α := +S.to_submonoid.mul_distrib_mul_action + +/-- The center of a group acts commutatively on that group. -/ +instance center.smul_comm_class_left : smul_comm_class (center G) G G := +submonoid.center.smul_comm_class_left + +/-- The center of a group acts commutatively on that group. -/ +instance center.smul_comm_class_right : smul_comm_class G (center G) G := +submonoid.center.smul_comm_class_right + +end subgroup diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean index a5c2c2982e21d..c84d3f099aae4 100644 --- a/src/group_theory/subgroup/basic.lean +++ b/src/group_theory/subgroup/basic.lean @@ -76,8 +76,6 @@ Definitions in the file: * `monoid_hom.eq_locus f g` : given group homomorphisms `f`, `g`, the elements of `G` such that `f x = g x` form a subgroup of `G` -* `is_simple_group G` : a class indicating that a group has exactly two normal subgroups - ## Implementation notes Subgroup inclusion is denoted `≤` rather than `⊆`, although `∈` is defined as @@ -2613,157 +2611,6 @@ hH.comap _ instance subgroup.normal_subgroup_of {H N : subgroup G} [N.normal] : (N.subgroup_of H).normal := subgroup.normal_comap _ -namespace subgroup - -/-- The subgroup generated by an element. -/ -def zpowers (g : G) : subgroup G := -subgroup.copy (zpowers_hom G g).range (set.range ((^) g : ℤ → G)) rfl - -@[simp] lemma mem_zpowers (g : G) : g ∈ zpowers g := ⟨1, zpow_one _⟩ - -lemma zpowers_eq_closure (g : G) : zpowers g = closure {g} := -by { ext, exact mem_closure_singleton.symm } - -@[simp] lemma range_zpowers_hom (g : G) : (zpowers_hom G g).range = zpowers g := rfl - -lemma zpowers_subset {a : G} {K : subgroup G} (h : a ∈ K) : zpowers a ≤ K := -λ x hx, match x, hx with _, ⟨i, rfl⟩ := K.zpow_mem h i end - -lemma mem_zpowers_iff {g h : G} : - h ∈ zpowers g ↔ ∃ (k : ℤ), g ^ k = h := -iff.rfl - -@[simp] lemma zpow_mem_zpowers (g : G) (k : ℤ) : g^k ∈ zpowers g := -mem_zpowers_iff.mpr ⟨k, rfl⟩ - -@[simp] lemma npow_mem_zpowers (g : G) (k : ℕ) : g^k ∈ zpowers g := -(zpow_coe_nat g k) ▸ zpow_mem_zpowers g k - -@[simp] lemma forall_zpowers {x : G} {p : zpowers x → Prop} : - (∀ g, p g) ↔ ∀ m : ℤ, p ⟨x ^ m, m, rfl⟩ := -set.forall_subtype_range_iff - -@[simp] lemma exists_zpowers {x : G} {p : zpowers x → Prop} : - (∃ g, p g) ↔ ∃ m : ℤ, p ⟨x ^ m, m, rfl⟩ := -set.exists_subtype_range_iff - -lemma forall_mem_zpowers {x : G} {p : G → Prop} : - (∀ g ∈ zpowers x, p g) ↔ ∀ m : ℤ, p (x ^ m) := -set.forall_range_iff - -lemma exists_mem_zpowers {x : G} {p : G → Prop} : - (∃ g ∈ zpowers x, p g) ↔ ∃ m : ℤ, p (x ^ m) := -set.exists_range_iff - -instance (a : G) : countable (zpowers a) := -((zpowers_hom G a).range_restrict_surjective.comp multiplicative.of_add.surjective).countable - -end subgroup - -namespace add_subgroup - -/-- The subgroup generated by an element. -/ -def zmultiples (a : A) : add_subgroup A := -add_subgroup.copy (zmultiples_hom A a).range (set.range ((• a) : ℤ → A)) rfl - -@[simp] lemma range_zmultiples_hom (a : A) : (zmultiples_hom A a).range = zmultiples a := rfl - -attribute [to_additive add_subgroup.zmultiples] subgroup.zpowers -attribute [to_additive add_subgroup.mem_zmultiples] subgroup.mem_zpowers -attribute [to_additive add_subgroup.zmultiples_eq_closure] subgroup.zpowers_eq_closure -attribute [to_additive add_subgroup.range_zmultiples_hom] subgroup.range_zpowers_hom -attribute [to_additive add_subgroup.zmultiples_subset] subgroup.zpowers_subset -attribute [to_additive add_subgroup.mem_zmultiples_iff] subgroup.mem_zpowers_iff -attribute [to_additive add_subgroup.zsmul_mem_zmultiples] subgroup.zpow_mem_zpowers -attribute [to_additive add_subgroup.nsmul_mem_zmultiples] subgroup.npow_mem_zpowers -attribute [to_additive add_subgroup.forall_zmultiples] subgroup.forall_zpowers -attribute [to_additive add_subgroup.forall_mem_zmultiples] subgroup.forall_mem_zpowers -attribute [to_additive add_subgroup.exists_zmultiples] subgroup.exists_zpowers -attribute [to_additive add_subgroup.exists_mem_zmultiples] subgroup.exists_mem_zpowers - -instance (a : A) : countable (zmultiples a) := -(zmultiples_hom A a).range_restrict_surjective.countable - -section ring - -variables {R : Type*} [ring R] (r : R) (k : ℤ) - -@[simp] lemma int_cast_mul_mem_zmultiples : - ↑(k : ℤ) * r ∈ zmultiples r := -by simpa only [← zsmul_eq_mul] using zsmul_mem_zmultiples r k - -@[simp] lemma int_cast_mem_zmultiples_one : - ↑(k : ℤ) ∈ zmultiples (1 : R) := -mem_zmultiples_iff.mp ⟨k, by simp⟩ - -end ring - -end add_subgroup - -@[simp, to_additive map_zmultiples] lemma monoid_hom.map_zpowers (f : G →* N) (x : G) : - (subgroup.zpowers x).map f = subgroup.zpowers (f x) := -by rw [subgroup.zpowers_eq_closure, subgroup.zpowers_eq_closure, f.map_closure, set.image_singleton] - -lemma int.mem_zmultiples_iff {a b : ℤ} : - b ∈ add_subgroup.zmultiples a ↔ a ∣ b := -exists_congr (λ k, by rw [mul_comm, eq_comm, ← smul_eq_mul]) - -lemma of_mul_image_zpowers_eq_zmultiples_of_mul { x : G } : - additive.of_mul '' ((subgroup.zpowers x) : set G) = add_subgroup.zmultiples (additive.of_mul x) := -begin - ext y, - split, - { rintro ⟨z, ⟨m, hm⟩, hz2⟩, - use m, - simp only, - rwa [← of_mul_zpow, hm] }, - { rintros ⟨n, hn⟩, - refine ⟨x ^ n, ⟨n, rfl⟩, _⟩, - rwa of_mul_zpow } -end - -lemma of_add_image_zmultiples_eq_zpowers_of_add {x : A} : - multiplicative.of_add '' ((add_subgroup.zmultiples x) : set A) = - subgroup.zpowers (multiplicative.of_add x) := -begin - symmetry, - rw equiv.eq_image_iff_symm_image_eq, - exact of_mul_image_zpowers_eq_zmultiples_of_mul, -end - -namespace subgroup - -@[to_additive zmultiples_is_commutative] -instance zpowers_is_commutative (g : G) : (zpowers g).is_commutative := -⟨⟨λ ⟨_, _, h₁⟩ ⟨_, _, h₂⟩, by rw [subtype.ext_iff, coe_mul, coe_mul, - subtype.coe_mk, subtype.coe_mk, ←h₁, ←h₂, zpow_mul_comm]⟩⟩ - -@[simp, to_additive zmultiples_le] -lemma zpowers_le {g : G} {H : subgroup G} : zpowers g ≤ H ↔ g ∈ H := -by rw [zpowers_eq_closure, closure_le, set.singleton_subset_iff, set_like.mem_coe] - -@[simp, to_additive zmultiples_eq_bot] lemma zpowers_eq_bot {g : G} : zpowers g = ⊥ ↔ g = 1 := -by rw [eq_bot_iff, zpowers_le, mem_bot] - -@[simp, to_additive zmultiples_zero_eq_bot] lemma zpowers_one_eq_bot : - subgroup.zpowers (1 : G) = ⊥ := -subgroup.zpowers_eq_bot.mpr rfl - -@[to_additive] lemma centralizer_closure (S : set G) : - (closure S).centralizer = ⨅ g ∈ S, (zpowers g).centralizer := -le_antisymm (le_infi $ λ g, le_infi $ λ hg, centralizer_le $ zpowers_le.2 $ subset_closure hg) - $ le_centralizer_iff.1 $ (closure_le _).2 - $ λ g, set_like.mem_coe.2 ∘ zpowers_le.1 ∘ le_centralizer_iff.1 ∘ infi_le_of_le g ∘ infi_le _ - -@[to_additive] lemma center_eq_infi (S : set G) (hS : closure S = ⊤) : - center G = ⨅ g ∈ S, centralizer (zpowers g) := -by rw [←centralizer_top, ←hS, centralizer_closure] - -@[to_additive] lemma center_eq_infi' (S : set G) (hS : closure S = ⊤) : - center G = ⨅ g : S, centralizer (zpowers g) := -by rw [center_eq_infi S hS, ←infi_subtype''] - -end subgroup namespace monoid_hom @@ -2857,49 +2704,6 @@ end⟩ end subgroup -section -variables (G) (A) - -/-- A `group` is simple when it has exactly two normal `subgroup`s. -/ -class is_simple_group extends nontrivial G : Prop := -(eq_bot_or_eq_top_of_normal : ∀ H : subgroup G, H.normal → H = ⊥ ∨ H = ⊤) - -/-- An `add_group` is simple when it has exactly two normal `add_subgroup`s. -/ -class is_simple_add_group extends nontrivial A : Prop := -(eq_bot_or_eq_top_of_normal : ∀ H : add_subgroup A, H.normal → H = ⊥ ∨ H = ⊤) - -attribute [to_additive] is_simple_group - -variables {G} {A} - -@[to_additive] -lemma subgroup.normal.eq_bot_or_eq_top [is_simple_group G] {H : subgroup G} (Hn : H.normal) : - H = ⊥ ∨ H = ⊤ := -is_simple_group.eq_bot_or_eq_top_of_normal H Hn - -namespace is_simple_group - -@[to_additive] -instance {C : Type*} [comm_group C] [is_simple_group C] : - is_simple_order (subgroup C) := -⟨λ H, H.normal_of_comm.eq_bot_or_eq_top⟩ - -open _root_.subgroup - -@[to_additive] -lemma is_simple_group_of_surjective {H : Type*} [group H] [is_simple_group G] - [nontrivial H] (f : G →* H) (hf : function.surjective f) : - is_simple_group H := -⟨nontrivial.exists_pair_ne, λ H iH, begin - refine ((iH.comap f).eq_bot_or_eq_top).imp (λ h, _) (λ h, _), - { rw [←map_bot f, ←h, map_comap_eq_self_of_surjective hf] }, - { rw [←comap_top f] at h, exact comap_injective hf h } -end⟩ - -end is_simple_group - -end - namespace subgroup section subgroup_normal @@ -3071,154 +2875,3 @@ begin end end is_conj - -/-! ### Actions by `subgroup`s - -These are just copies of the definitions about `submonoid` starting from `submonoid.mul_action`. --/ -section actions - -namespace subgroup - -variables {α β : Type*} - -/-- The action by a subgroup is the action by the underlying group. -/ -@[to_additive /-"The additive action by an add_subgroup is the action by the underlying -add_group. "-/] -instance [mul_action G α] (S : subgroup G) : mul_action S α := -S.to_submonoid.mul_action - -@[to_additive] -lemma smul_def [mul_action G α] {S : subgroup G} (g : S) (m : α) : g • m = (g : G) • m := rfl - -@[to_additive] -instance smul_comm_class_left - [mul_action G β] [has_smul α β] [smul_comm_class G α β] (S : subgroup G) : - smul_comm_class S α β := -S.to_submonoid.smul_comm_class_left - -@[to_additive] -instance smul_comm_class_right - [has_smul α β] [mul_action G β] [smul_comm_class α G β] (S : subgroup G) : - smul_comm_class α S β := -S.to_submonoid.smul_comm_class_right - -/-- Note that this provides `is_scalar_tower S G G` which is needed by `smul_mul_assoc`. -/ -instance - [has_smul α β] [mul_action G α] [mul_action G β] [is_scalar_tower G α β] (S : subgroup G) : - is_scalar_tower S α β := -S.to_submonoid.is_scalar_tower - -instance [mul_action G α] [has_faithful_smul G α] (S : subgroup G) : - has_faithful_smul S α := -S.to_submonoid.has_faithful_smul - -/-- The action by a subgroup is the action by the underlying group. -/ -instance [add_monoid α] [distrib_mul_action G α] (S : subgroup G) : distrib_mul_action S α := -S.to_submonoid.distrib_mul_action - -/-- The action by a subgroup is the action by the underlying group. -/ -instance [monoid α] [mul_distrib_mul_action G α] (S : subgroup G) : mul_distrib_mul_action S α := -S.to_submonoid.mul_distrib_mul_action - -/-- The center of a group acts commutatively on that group. -/ -instance center.smul_comm_class_left : smul_comm_class (center G) G G := -submonoid.center.smul_comm_class_left - -/-- The center of a group acts commutatively on that group. -/ -instance center.smul_comm_class_right : smul_comm_class G (center G) G := -submonoid.center.smul_comm_class_right - -end subgroup - -end actions - -/-! ### Mul-opposite subgroups -/ - -section mul_opposite - -namespace subgroup - -/-- A subgroup `H` of `G` determines a subgroup `H.opposite` of the opposite group `Gᵐᵒᵖ`. -/ -@[to_additive "An additive subgroup `H` of `G` determines an additive subgroup `H.opposite` of the - opposite additive group `Gᵃᵒᵖ`."] -def opposite : subgroup G ≃ subgroup Gᵐᵒᵖ := -{ to_fun := λ H, { carrier := mul_opposite.unop ⁻¹' (H : set G), - one_mem' := H.one_mem, - mul_mem' := λ a b ha hb, H.mul_mem hb ha, - inv_mem' := λ a, H.inv_mem }, - inv_fun := λ H, { carrier := mul_opposite.op ⁻¹' (H : set Gᵐᵒᵖ), - one_mem' := H.one_mem, - mul_mem' := λ a b ha hb, H.mul_mem hb ha, - inv_mem' := λ a, H.inv_mem }, - left_inv := λ H, set_like.coe_injective rfl, - right_inv := λ H, set_like.coe_injective rfl } - -/-- Bijection between a subgroup `H` and its opposite. -/ -@[to_additive "Bijection between an additive subgroup `H` and its opposite.", simps] -def opposite_equiv (H : subgroup G) : H ≃ H.opposite := -mul_opposite.op_equiv.subtype_equiv $ λ _, iff.rfl - -@[to_additive] instance (H : subgroup G) [encodable H] : encodable H.opposite := -encodable.of_equiv H H.opposite_equiv.symm - -@[to_additive] instance (H : subgroup G) [countable H] : countable H.opposite := -countable.of_equiv H H.opposite_equiv - -@[to_additive] lemma smul_opposite_mul {H : subgroup G} (x g : G) (h : H.opposite) : - h • (g * x) = g * (h • x) := -begin - cases h, - simp [(•), mul_assoc], -end - -end subgroup - -end mul_opposite - -/-! ### Saturated subgroups -/ - -section saturated - -namespace subgroup - -/-- A subgroup `H` of `G` is *saturated* if for all `n : ℕ` and `g : G` with `g^n ∈ H` -we have `n = 0` or `g ∈ H`. -/ -@[to_additive "An additive subgroup `H` of `G` is *saturated* if -for all `n : ℕ` and `g : G` with `n•g ∈ H` we have `n = 0` or `g ∈ H`."] -def saturated (H : subgroup G) : Prop := ∀ ⦃n g⦄, g ^ n ∈ H → n = 0 ∨ g ∈ H - -@[to_additive] lemma saturated_iff_npow {H : subgroup G} : - saturated H ↔ (∀ (n : ℕ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H) := iff.rfl - -@[to_additive] lemma saturated_iff_zpow {H : subgroup G} : - saturated H ↔ (∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H) := -begin - split, - { rintros hH ⟨n⟩ g hgn, - { simp only [int.coe_nat_eq_zero, int.of_nat_eq_coe, zpow_coe_nat] at hgn ⊢, - exact hH hgn }, - { suffices : g ^ (n+1) ∈ H, - { refine (hH this).imp _ id, simp only [is_empty.forall_iff, nat.succ_ne_zero], }, - simpa only [inv_mem_iff, zpow_neg_succ_of_nat] using hgn, } }, - { intros h n g hgn, - specialize h n g, - simp only [int.coe_nat_eq_zero, zpow_coe_nat] at h, - apply h hgn } -end - -end subgroup - -namespace add_subgroup - -lemma ker_saturated {A₁ A₂ : Type*} [add_comm_group A₁] [add_comm_group A₂] - [no_zero_smul_divisors ℕ A₂] (f : A₁ →+ A₂) : - (f.ker).saturated := -begin - intros n g hg, - simpa only [f.mem_ker, nsmul_eq_smul, f.map_nsmul, smul_eq_zero] using hg -end - -end add_subgroup - -end saturated diff --git a/src/group_theory/subgroup/mul_opposite.lean b/src/group_theory/subgroup/mul_opposite.lean new file mode 100644 index 0000000000000..93f590238c684 --- /dev/null +++ b/src/group_theory/subgroup/mul_opposite.lean @@ -0,0 +1,54 @@ +/- +Copyright (c) 2022 Alex Kontorovich. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alex Kontorovich +-/ + +import group_theory.subgroup.actions + +/-! +# Mul-opposite subgroups + +## Tags +subgroup, subgroups + +-/ + +variables {G : Type*} [group G] + +namespace subgroup + +/-- A subgroup `H` of `G` determines a subgroup `H.opposite` of the opposite group `Gᵐᵒᵖ`. -/ +@[to_additive "An additive subgroup `H` of `G` determines an additive subgroup `H.opposite` of the + opposite additive group `Gᵃᵒᵖ`."] +def opposite : subgroup G ≃ subgroup Gᵐᵒᵖ := +{ to_fun := λ H, { carrier := mul_opposite.unop ⁻¹' (H : set G), + one_mem' := H.one_mem, + mul_mem' := λ a b ha hb, H.mul_mem hb ha, + inv_mem' := λ a, H.inv_mem }, + inv_fun := λ H, { carrier := mul_opposite.op ⁻¹' (H : set Gᵐᵒᵖ), + one_mem' := H.one_mem, + mul_mem' := λ a b ha hb, H.mul_mem hb ha, + inv_mem' := λ a, H.inv_mem }, + left_inv := λ H, set_like.coe_injective rfl, + right_inv := λ H, set_like.coe_injective rfl } + +/-- Bijection between a subgroup `H` and its opposite. -/ +@[to_additive "Bijection between an additive subgroup `H` and its opposite.", simps] +def opposite_equiv (H : subgroup G) : H ≃ H.opposite := +mul_opposite.op_equiv.subtype_equiv $ λ _, iff.rfl + +@[to_additive] instance (H : subgroup G) [encodable H] : encodable H.opposite := +encodable.of_equiv H H.opposite_equiv.symm + +@[to_additive] instance (H : subgroup G) [countable H] : countable H.opposite := +countable.of_equiv H H.opposite_equiv + +@[to_additive] lemma smul_opposite_mul {H : subgroup G} (x g : G) (h : H.opposite) : + h • (g * x) = g * (h • x) := +begin + cases h, + simp [(•), mul_assoc], +end + +end subgroup diff --git a/src/group_theory/subgroup/pointwise.lean b/src/group_theory/subgroup/pointwise.lean index 67d21096238a2..3a565dfb0313f 100644 --- a/src/group_theory/subgroup/pointwise.lean +++ b/src/group_theory/subgroup/pointwise.lean @@ -3,7 +3,7 @@ Copyright (c) 2021 Eric Wieser. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Wieser -/ -import group_theory.subgroup.basic +import group_theory.subgroup.mul_opposite import group_theory.submonoid.pointwise import group_theory.group_action.conj_act diff --git a/src/group_theory/subgroup/saturated.lean b/src/group_theory/subgroup/saturated.lean new file mode 100644 index 0000000000000..e22b4921d7165 --- /dev/null +++ b/src/group_theory/subgroup/saturated.lean @@ -0,0 +1,58 @@ +/- +Copyright (c) 2021 Johan Commelin. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johan Commelin +-/ + +import group_theory.subgroup.basic + +/-! +# Saturated subgroups + +## Tags +subgroup, subgroups + +-/ + +namespace subgroup + +variables {G : Type*} [group G] + +/-- A subgroup `H` of `G` is *saturated* if for all `n : ℕ` and `g : G` with `g^n ∈ H` +we have `n = 0` or `g ∈ H`. -/ +@[to_additive "An additive subgroup `H` of `G` is *saturated* if +for all `n : ℕ` and `g : G` with `n•g ∈ H` we have `n = 0` or `g ∈ H`."] +def saturated (H : subgroup G) : Prop := ∀ ⦃n g⦄, g ^ n ∈ H → n = 0 ∨ g ∈ H + +@[to_additive] lemma saturated_iff_npow {H : subgroup G} : + saturated H ↔ (∀ (n : ℕ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H) := iff.rfl + +@[to_additive] lemma saturated_iff_zpow {H : subgroup G} : + saturated H ↔ (∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H) := +begin + split, + { rintros hH ⟨n⟩ g hgn, + { simp only [int.coe_nat_eq_zero, int.of_nat_eq_coe, zpow_coe_nat] at hgn ⊢, + exact hH hgn }, + { suffices : g ^ (n+1) ∈ H, + { refine (hH this).imp _ id, simp only [is_empty.forall_iff, nat.succ_ne_zero], }, + simpa only [inv_mem_iff, zpow_neg_succ_of_nat] using hgn, } }, + { intros h n g hgn, + specialize h n g, + simp only [int.coe_nat_eq_zero, zpow_coe_nat] at h, + apply h hgn } +end + +end subgroup + +namespace add_subgroup + +lemma ker_saturated {A₁ A₂ : Type*} [add_comm_group A₁] [add_comm_group A₂] + [no_zero_smul_divisors ℕ A₂] (f : A₁ →+ A₂) : + (f.ker).saturated := +begin + intros n g hg, + simpa only [f.mem_ker, nsmul_eq_smul, f.map_nsmul, smul_eq_zero] using hg +end + +end add_subgroup diff --git a/src/group_theory/subgroup/simple.lean b/src/group_theory/subgroup/simple.lean new file mode 100644 index 0000000000000..f043081c9206e --- /dev/null +++ b/src/group_theory/subgroup/simple.lean @@ -0,0 +1,70 @@ +/- +Copyright (c) 2021 Aaron Anderson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Aaron Anderson +-/ + +import group_theory.subgroup.actions + +/-! +# Simple groups + +This file defines `is_simple_group G`, a class indicating that a group has exactly two normal +subgroups. + +## Main definitions + +- `is_simple_group G`, a class indicating that a group has exactly two normal subgroups. + +## Tags +subgroup, subgroups + +-/ + +set_option old_structure_cmd true + +variables {G : Type*} [group G] +variables {A : Type*} [add_group A] + +section +variables (G) (A) + +/-- A `group` is simple when it has exactly two normal `subgroup`s. -/ +class is_simple_group extends nontrivial G : Prop := +(eq_bot_or_eq_top_of_normal : ∀ H : subgroup G, H.normal → H = ⊥ ∨ H = ⊤) + +/-- An `add_group` is simple when it has exactly two normal `add_subgroup`s. -/ +class is_simple_add_group extends nontrivial A : Prop := +(eq_bot_or_eq_top_of_normal : ∀ H : add_subgroup A, H.normal → H = ⊥ ∨ H = ⊤) + +attribute [to_additive] is_simple_group + +variables {G} {A} + +@[to_additive] +lemma subgroup.normal.eq_bot_or_eq_top [is_simple_group G] {H : subgroup G} (Hn : H.normal) : + H = ⊥ ∨ H = ⊤ := +is_simple_group.eq_bot_or_eq_top_of_normal H Hn + +namespace is_simple_group + +@[to_additive] +instance {C : Type*} [comm_group C] [is_simple_group C] : + is_simple_order (subgroup C) := +⟨λ H, H.normal_of_comm.eq_bot_or_eq_top⟩ + +open _root_.subgroup + +@[to_additive] +lemma is_simple_group_of_surjective {H : Type*} [group H] [is_simple_group G] + [nontrivial H] (f : G →* H) (hf : function.surjective f) : + is_simple_group H := +⟨nontrivial.exists_pair_ne, λ H iH, begin + refine ((iH.comap f).eq_bot_or_eq_top).imp (λ h, _) (λ h, _), + { rw [←map_bot f, ←h, map_comap_eq_self_of_surjective hf] }, + { rw [←comap_top f] at h, exact comap_injective hf h } +end⟩ + +end is_simple_group + +end diff --git a/src/group_theory/subgroup/zpowers.lean b/src/group_theory/subgroup/zpowers.lean new file mode 100644 index 0000000000000..b7a89fb456edd --- /dev/null +++ b/src/group_theory/subgroup/zpowers.lean @@ -0,0 +1,171 @@ +/- +Copyright (c) 2020 Chris Hughes. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Hughes +-/ + +import group_theory.subgroup.basic + +/-! +# Subgroups generated by an element + +## Tags +subgroup, subgroups + +-/ + +variables {G : Type*} [group G] +variables {A : Type*} [add_group A] +variables {N : Type*} [group N] + +namespace subgroup + +/-- The subgroup generated by an element. -/ +def zpowers (g : G) : subgroup G := +subgroup.copy (zpowers_hom G g).range (set.range ((^) g : ℤ → G)) rfl + +@[simp] lemma mem_zpowers (g : G) : g ∈ zpowers g := ⟨1, zpow_one _⟩ + +lemma zpowers_eq_closure (g : G) : zpowers g = closure {g} := +by { ext, exact mem_closure_singleton.symm } + +@[simp] lemma range_zpowers_hom (g : G) : (zpowers_hom G g).range = zpowers g := rfl + +lemma zpowers_subset {a : G} {K : subgroup G} (h : a ∈ K) : zpowers a ≤ K := +λ x hx, match x, hx with _, ⟨i, rfl⟩ := K.zpow_mem h i end + +lemma mem_zpowers_iff {g h : G} : + h ∈ zpowers g ↔ ∃ (k : ℤ), g ^ k = h := +iff.rfl + +@[simp] lemma zpow_mem_zpowers (g : G) (k : ℤ) : g^k ∈ zpowers g := +mem_zpowers_iff.mpr ⟨k, rfl⟩ + +@[simp] lemma npow_mem_zpowers (g : G) (k : ℕ) : g^k ∈ zpowers g := +(zpow_coe_nat g k) ▸ zpow_mem_zpowers g k + +@[simp] lemma forall_zpowers {x : G} {p : zpowers x → Prop} : + (∀ g, p g) ↔ ∀ m : ℤ, p ⟨x ^ m, m, rfl⟩ := +set.forall_subtype_range_iff + +@[simp] lemma exists_zpowers {x : G} {p : zpowers x → Prop} : + (∃ g, p g) ↔ ∃ m : ℤ, p ⟨x ^ m, m, rfl⟩ := +set.exists_subtype_range_iff + +lemma forall_mem_zpowers {x : G} {p : G → Prop} : + (∀ g ∈ zpowers x, p g) ↔ ∀ m : ℤ, p (x ^ m) := +set.forall_range_iff + +lemma exists_mem_zpowers {x : G} {p : G → Prop} : + (∃ g ∈ zpowers x, p g) ↔ ∃ m : ℤ, p (x ^ m) := +set.exists_range_iff + +instance (a : G) : countable (zpowers a) := +((zpowers_hom G a).range_restrict_surjective.comp multiplicative.of_add.surjective).countable + +end subgroup + +namespace add_subgroup + +/-- The subgroup generated by an element. -/ +def zmultiples (a : A) : add_subgroup A := +add_subgroup.copy (zmultiples_hom A a).range (set.range ((• a) : ℤ → A)) rfl + +@[simp] lemma range_zmultiples_hom (a : A) : (zmultiples_hom A a).range = zmultiples a := rfl + +attribute [to_additive add_subgroup.zmultiples] subgroup.zpowers +attribute [to_additive add_subgroup.mem_zmultiples] subgroup.mem_zpowers +attribute [to_additive add_subgroup.zmultiples_eq_closure] subgroup.zpowers_eq_closure +attribute [to_additive add_subgroup.range_zmultiples_hom] subgroup.range_zpowers_hom +attribute [to_additive add_subgroup.zmultiples_subset] subgroup.zpowers_subset +attribute [to_additive add_subgroup.mem_zmultiples_iff] subgroup.mem_zpowers_iff +attribute [to_additive add_subgroup.zsmul_mem_zmultiples] subgroup.zpow_mem_zpowers +attribute [to_additive add_subgroup.nsmul_mem_zmultiples] subgroup.npow_mem_zpowers +attribute [to_additive add_subgroup.forall_zmultiples] subgroup.forall_zpowers +attribute [to_additive add_subgroup.forall_mem_zmultiples] subgroup.forall_mem_zpowers +attribute [to_additive add_subgroup.exists_zmultiples] subgroup.exists_zpowers +attribute [to_additive add_subgroup.exists_mem_zmultiples] subgroup.exists_mem_zpowers + +instance (a : A) : countable (zmultiples a) := +(zmultiples_hom A a).range_restrict_surjective.countable + +section ring + +variables {R : Type*} [ring R] (r : R) (k : ℤ) + +@[simp] lemma int_cast_mul_mem_zmultiples : + ↑(k : ℤ) * r ∈ zmultiples r := +by simpa only [← zsmul_eq_mul] using zsmul_mem_zmultiples r k + +@[simp] lemma int_cast_mem_zmultiples_one : + ↑(k : ℤ) ∈ zmultiples (1 : R) := +mem_zmultiples_iff.mp ⟨k, by simp⟩ + +end ring + +end add_subgroup + +@[simp, to_additive map_zmultiples] lemma monoid_hom.map_zpowers (f : G →* N) (x : G) : + (subgroup.zpowers x).map f = subgroup.zpowers (f x) := +by rw [subgroup.zpowers_eq_closure, subgroup.zpowers_eq_closure, f.map_closure, set.image_singleton] + +lemma int.mem_zmultiples_iff {a b : ℤ} : + b ∈ add_subgroup.zmultiples a ↔ a ∣ b := +exists_congr (λ k, by rw [mul_comm, eq_comm, ← smul_eq_mul]) + +lemma of_mul_image_zpowers_eq_zmultiples_of_mul { x : G } : + additive.of_mul '' ((subgroup.zpowers x) : set G) = add_subgroup.zmultiples (additive.of_mul x) := +begin + ext y, + split, + { rintro ⟨z, ⟨m, hm⟩, hz2⟩, + use m, + simp only, + rwa [← of_mul_zpow, hm] }, + { rintros ⟨n, hn⟩, + refine ⟨x ^ n, ⟨n, rfl⟩, _⟩, + rwa of_mul_zpow } +end + +lemma of_add_image_zmultiples_eq_zpowers_of_add {x : A} : + multiplicative.of_add '' ((add_subgroup.zmultiples x) : set A) = + subgroup.zpowers (multiplicative.of_add x) := +begin + symmetry, + rw equiv.eq_image_iff_symm_image_eq, + exact of_mul_image_zpowers_eq_zmultiples_of_mul, +end + +namespace subgroup + +@[to_additive zmultiples_is_commutative] +instance zpowers_is_commutative (g : G) : (zpowers g).is_commutative := +⟨⟨λ ⟨_, _, h₁⟩ ⟨_, _, h₂⟩, by rw [subtype.ext_iff, coe_mul, coe_mul, + subtype.coe_mk, subtype.coe_mk, ←h₁, ←h₂, zpow_mul_comm]⟩⟩ + +@[simp, to_additive zmultiples_le] +lemma zpowers_le {g : G} {H : subgroup G} : zpowers g ≤ H ↔ g ∈ H := +by rw [zpowers_eq_closure, closure_le, set.singleton_subset_iff, set_like.mem_coe] + +@[simp, to_additive zmultiples_eq_bot] lemma zpowers_eq_bot {g : G} : zpowers g = ⊥ ↔ g = 1 := +by rw [eq_bot_iff, zpowers_le, mem_bot] + +@[simp, to_additive zmultiples_zero_eq_bot] lemma zpowers_one_eq_bot : + subgroup.zpowers (1 : G) = ⊥ := +subgroup.zpowers_eq_bot.mpr rfl + +@[to_additive] lemma centralizer_closure (S : set G) : + (closure S).centralizer = ⨅ g ∈ S, (zpowers g).centralizer := +le_antisymm (le_infi $ λ g, le_infi $ λ hg, centralizer_le $ zpowers_le.2 $ subset_closure hg) + $ le_centralizer_iff.1 $ (closure_le _).2 + $ λ g, set_like.mem_coe.2 ∘ zpowers_le.1 ∘ le_centralizer_iff.1 ∘ infi_le_of_le g ∘ infi_le _ + +@[to_additive] lemma center_eq_infi (S : set G) (hS : closure S = ⊤) : + center G = ⨅ g ∈ S, centralizer (zpowers g) := +by rw [←centralizer_top, ←hS, centralizer_closure] + +@[to_additive] lemma center_eq_infi' (S : set G) (hS : closure S = ⊤) : + center G = ⨅ g : S, centralizer (zpowers g) := +by rw [center_eq_infi S hS, ←infi_subtype''] + +end subgroup diff --git a/src/linear_algebra/ray.lean b/src/linear_algebra/ray.lean index 9d9a2801a262f..c12aec99af056 100644 --- a/src/linear_algebra/ray.lean +++ b/src/linear_algebra/ray.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Joseph Myers. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Myers -/ +import group_theory.subgroup.actions import linear_algebra.linear_independent /-!