From 515fb2f01c2abdcff77ae61b919c5e3a706b69f0 Mon Sep 17 00:00:00 2001 From: Aaron Anderson Date: Fri, 7 May 2021 22:54:25 +0000 Subject: [PATCH] feat(group_theory/perm/*): lemmas about `extend_domain`, `fin_rotate`, and `fin.cycle_type` (#7447) Shows how `disjoint`, `support`, `is_cycle`, and `cycle_type` behave under `extend_domain` Calculates `support` and `cycle_type` for `fin_rotate` and `fin.cycle_type` Shows that the normal closure of `fin_rotate 5` in `alternating_group (fin 5)` is the whole alternating group. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com> --- src/analysis/normed_space/hahn_banach.lean | 9 +- src/group_theory/perm/cycle_type.lean | 12 +++ src/group_theory/perm/cycles.lean | 25 ++++++ src/group_theory/perm/fin.lean | 70 +++++++++++++++ src/group_theory/perm/sign.lean | 13 +++ src/group_theory/perm/support.lean | 36 ++++++++ .../specific_groups/alternating.lean | 86 ++++++++++++++++++- src/group_theory/subgroup.lean | 3 + src/linear_algebra/bilinear_form.lean | 9 +- 9 files changed, 252 insertions(+), 11 deletions(-) diff --git a/src/analysis/normed_space/hahn_banach.lean b/src/analysis/normed_space/hahn_banach.lean index acda574ebae07..a59a990d4d10a 100644 --- a/src/analysis/normed_space/hahn_banach.lean +++ b/src/analysis/normed_space/hahn_banach.lean @@ -89,7 +89,7 @@ begin -- we'll call `g : F →L[ℝ] ℝ`. rcases real.exists_extension_norm_eq (p.restrict_scalars ℝ) fr with ⟨g, ⟨hextends, hnormeq⟩⟩, -- Now `g` can be extended to the `F →L[𝕜] 𝕜` we need. - use g.extend_to_𝕜, + refine ⟨g.extend_to_𝕜, _⟩, -- It is an extension of `f`. have h : ∀ x : p, g.extend_to_𝕜 x = f x, { assume x, @@ -104,15 +104,14 @@ begin { simp only [algebra.id.smul_eq_mul, I_re, of_real_im, add_monoid_hom.map_add, zero_sub, I_im', zero_mul, of_real_re, mul_neg_eq_neg_mul_symm, mul_im, zero_add, of_real_neg, mul_re, sub_neg_eq_add, continuous_linear_map.map_smul] } }, - refine ⟨h, _⟩, -- And we derive the equality of the norms by bounding on both sides. - refine le_antisymm _ _, + refine ⟨h, le_antisymm _ _⟩, { calc ∥g.extend_to_𝕜∥ ≤ ∥g∥ : g.extend_to_𝕜.op_norm_le_bound g.op_norm_nonneg (norm_bound _) ... = ∥fr∥ : hnormeq ... ≤ ∥re_clm∥ * ∥f∥ : continuous_linear_map.op_norm_comp_le _ _ ... = ∥f∥ : by rw [re_clm_norm, one_mul] }, - { exact f.op_norm_le_bound g.extend_to_𝕜.op_norm_nonneg (λ x, h x ▸ g.extend_to_𝕜.le_op_norm x) }, + { exact f.op_norm_le_bound g.extend_to_𝕜.op_norm_nonneg (λ x, h x ▸ g.extend_to_𝕜.le_op_norm x) } end end is_R_or_C @@ -134,7 +133,7 @@ begin let p : submodule 𝕜 E := 𝕜 ∙ x, let f := norm' 𝕜 x • coord 𝕜 x h, obtain ⟨g, hg⟩ := exists_extension_norm_eq p f, - use g, split, + refine ⟨g, _, _⟩, { rw [hg.2, coord_norm'] }, { calc g x = g (⟨x, mem_span_singleton_self x⟩ : 𝕜 ∙ x) : by rw coe_mk ... = (norm' 𝕜 x • coord 𝕜 x h) (⟨x, mem_span_singleton_self x⟩ : 𝕜 ∙ x) : by rw ← hg.1 diff --git a/src/group_theory/perm/cycle_type.lean b/src/group_theory/perm/cycle_type.lean index 7a65674dc384f..95efb9cd676f5 100644 --- a/src/group_theory/perm/cycle_type.lean +++ b/src/group_theory/perm/cycle_type.lean @@ -269,6 +269,18 @@ theorem is_conj_iff_cycle_type_eq {σ τ : perm α} : rw cycle_type_conj, end, is_conj_of_cycle_type_eq⟩ +@[simp] lemma cycle_type_extend_domain {β : Type*} [fintype β] [decidable_eq β] + {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) {g : perm α} : + cycle_type (g.extend_domain f) = cycle_type g := +begin + apply cycle_induction_on _ g, + { rw [extend_domain_one, cycle_type_one, cycle_type_one] }, + { intros σ hσ, + rw [(hσ.extend_domain f).cycle_type, hσ.cycle_type, card_support_extend_domain] }, + { intros σ τ hd hc hσ hτ, + rw [hd.cycle_type, ← extend_domain_mul, (hd.extend_domain f).cycle_type, hσ, hτ] } +end + end cycle_type lemma is_cycle_of_prime_order' {σ : perm α} (h1 : (order_of σ).prime) diff --git a/src/group_theory/perm/cycles.lean b/src/group_theory/perm/cycles.lean index e9e4b58416c25..028cfbfa04764 100644 --- a/src/group_theory/perm/cycles.lean +++ b/src/group_theory/perm/cycles.lean @@ -259,6 +259,31 @@ begin exact ⟨n * i, by rwa gpow_mul⟩, end +lemma is_cycle.extend_domain {α : Type*} {p : β → Prop} [decidable_pred p] + (f : α ≃ subtype p) {g : perm α} (h : is_cycle g) : + is_cycle (g.extend_domain f) := +begin + obtain ⟨a, ha, ha'⟩ := h, + refine ⟨f a, _, λ b hb, _⟩, + { rw extend_domain_apply_image, + exact λ con, ha (f.injective (subtype.coe_injective con)) }, + by_cases pb : p b, + { obtain ⟨i, hi⟩ := ha' (f.symm ⟨b, pb⟩) (λ con, hb _), + { refine ⟨i, _⟩, + have hnat : ∀ (k : ℕ) (a : α), (g.extend_domain f ^ k) ↑(f a) = f ((g ^ k) a), + { intros k a, + induction k with k ih, { refl }, + rw [pow_succ, perm.mul_apply, ih, extend_domain_apply_image, pow_succ, perm.mul_apply] }, + have hint : ∀ (k : ℤ) (a : α), (g.extend_domain f ^ k) ↑(f a) = f ((g ^ k) a), + { intros k a, + induction k with k k, + { rw [gpow_of_nat, gpow_of_nat, hnat] }, + rw [gpow_neg_succ_of_nat, gpow_neg_succ_of_nat, inv_eq_iff_eq, hnat, apply_inv_self] }, + rw [hint, hi, apply_symm_apply, subtype.coe_mk] }, + { rw [extend_domain_apply_subtype _ _ pb, con, apply_symm_apply, subtype.coe_mk] } }, + { exact (hb (extend_domain_apply_not_subtype _ _ pb)).elim } +end + end sign_cycle /-! diff --git a/src/group_theory/perm/fin.lean b/src/group_theory/perm/fin.lean index cf1e1d2e0df2d..59f152085f743 100644 --- a/src/group_theory/perm/fin.lean +++ b/src/group_theory/perm/fin.lean @@ -6,6 +6,7 @@ Authors: Eric Wieser import data.equiv.fin import data.equiv.fintype import group_theory.perm.option +import group_theory.perm.cycle_type /-! # Permutations of `fin n` @@ -95,6 +96,49 @@ begin { rw fin_rotate_succ, simp [ih, pow_succ] }, end +@[simp] lemma support_fin_rotate {n : ℕ} : support (fin_rotate (n + 2)) = finset.univ := +by { ext, simp } + +lemma support_fin_rotate_of_le {n : ℕ} (h : 2 ≤ n) : + support (fin_rotate n) = finset.univ := +begin + obtain ⟨m, rfl⟩ := exists_add_of_le h, + rw [add_comm, support_fin_rotate], +end + +lemma is_cycle_fin_rotate {n : ℕ} : is_cycle (fin_rotate (n + 2)) := +begin + refine ⟨0, dec_trivial, λ x hx', ⟨x, _⟩⟩, + clear hx', + cases x with x hx, + rw [coe_coe, gpow_coe_nat, fin.ext_iff, fin.coe_mk], + induction x with x ih, { refl }, + rw [pow_succ, perm.mul_apply, coe_fin_rotate_of_ne_last, ih (lt_trans x.lt_succ_self hx)], + rw [ne.def, fin.ext_iff, ih (lt_trans x.lt_succ_self hx), fin.coe_last], + exact ne_of_lt (nat.lt_of_succ_lt_succ hx), +end + +lemma is_cycle_fin_rotate_of_le {n : ℕ} (h : 2 ≤ n) : + is_cycle (fin_rotate n) := +begin + obtain ⟨m, rfl⟩ := exists_add_of_le h, + rw [add_comm], + exact is_cycle_fin_rotate +end + +@[simp] lemma cycle_type_fin_rotate {n : ℕ} : cycle_type (fin_rotate (n + 2)) = {n + 2} := +begin + rw [is_cycle_fin_rotate.cycle_type, support_fin_rotate, ← fintype.card, fintype.card_fin], + refl, +end + +lemma cycle_type_fin_rotate_of_le {n : ℕ} (h : 2 ≤ n) : + cycle_type (fin_rotate n) = {n} := +begin + obtain ⟨m, rfl⟩ := exists_add_of_le h, + rw [add_comm, cycle_type_fin_rotate] +end + namespace fin /-- `fin.cycle_range i` is the cycle `(0 1 2 ... i)` leaving `(i+1 ... (n-1))` unchanged. -/ @@ -226,6 +270,32 @@ i.cycle_range.injective (by simp) i.cycle_range.symm j.succ = i.succ_above j := i.cycle_range.injective (by simp) +lemma is_cycle_cycle_range {n : ℕ} {i : fin (n + 1)} (h0 : i ≠ 0) : is_cycle (cycle_range i) := +begin + cases i with i hi, + cases i, + { exact (h0 rfl).elim }, + exact is_cycle_fin_rotate.extend_domain _, +end + +@[simp] lemma cycle_type_cycle_range {n : ℕ} {i : fin (n + 1)} (h0 : i ≠ 0) : + cycle_type (cycle_range i) = {i + 1} := +begin + cases i with i hi, + cases i, + { exact (h0 rfl).elim }, + rw [cycle_range, cycle_type_extend_domain], + exact cycle_type_fin_rotate, +end + +lemma is_three_cycle_cycle_range_two {n : ℕ} : + is_three_cycle (cycle_range 2 : perm (fin (n + 3))) := +begin + rw [is_three_cycle, cycle_type_cycle_range, multiset.singleton_eq_singleton, + multiset.singleton_eq_singleton, multiset.cons_inj_left]; + dec_trivial +end + end fin end cycle_range diff --git a/src/group_theory/perm/sign.lean b/src/group_theory/perm/sign.lean index 85d87e813546d..da570df84459a 100644 --- a/src/group_theory/perm/sign.lean +++ b/src/group_theory/perm/sign.lean @@ -151,6 +151,19 @@ begin (order_of_dvd_of_pow_eq_one ((h (order_of (σ * τ))).mp (pow_order_of_eq_one (σ * τ))).2)), end +lemma disjoint.extend_domain {α : Type*} {p : β → Prop} [decidable_pred p] + (f : α ≃ subtype p) {σ τ : perm α} (h : disjoint σ τ) : + disjoint (σ.extend_domain f) (τ.extend_domain f) := +begin + intro b, + by_cases pb : p b, + { refine (h (f.symm ⟨b, pb⟩)).imp _ _; + { intro h, + rw [extend_domain_apply_subtype _ _ pb, h, apply_symm_apply, subtype.coe_mk] } }, + { left, + rw [extend_domain_apply_not_subtype _ _ pb] } +end + variable [decidable_eq α] section fintype diff --git a/src/group_theory/perm/support.lean b/src/group_theory/perm/support.lean index f2c5b68973583..92082252d0b6c 100644 --- a/src/group_theory/perm/support.lean +++ b/src/group_theory/perm/support.lean @@ -389,6 +389,42 @@ begin { split_ifs at hy; cc } end +section extend_domain +variables {β : Type*} [decidable_eq β] [fintype β] {p : β → Prop} [decidable_pred p] + +@[simp] +lemma support_extend_domain (f : α ≃ subtype p) {g : perm α} : + support (g.extend_domain f) = g.support.map f.as_embedding := +begin + ext b, + simp only [exists_prop, function.embedding.coe_fn_mk, to_embedding_apply, mem_map, ne.def, + function.embedding.trans_apply, mem_support], + by_cases pb : p b, + { rw [extend_domain_apply_subtype _ _ pb], + split, + { rintro h, + refine ⟨f.symm ⟨b, pb⟩, _, by simp⟩, + contrapose! h, + simp [h] }, + { rintro ⟨a, ha, hb⟩, + contrapose! ha, + obtain rfl : a = f.symm ⟨b, pb⟩, + { rw eq_symm_apply, + exact subtype.coe_injective hb }, + rw eq_symm_apply, + exact subtype.coe_injective ha } }, + { rw [extend_domain_apply_not_subtype _ _ pb], + simp only [not_exists, false_iff, not_and, eq_self_iff_true, not_true], + rintros a ha rfl, + exact pb (subtype.prop _) } +end + +lemma card_support_extend_domain (f : α ≃ subtype p) {g : perm α} : + (g.extend_domain f).support.card = g.support.card := +by simp + +end extend_domain + section card @[simp] diff --git a/src/group_theory/specific_groups/alternating.lean b/src/group_theory/specific_groups/alternating.lean index 6ea1d58ef8edf..16a471e661f0c 100644 --- a/src/group_theory/specific_groups/alternating.lean +++ b/src/group_theory/specific_groups/alternating.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Aaron Anderson -/ -import group_theory.perm.cycle_type +import group_theory.perm.fin /-! # Alternating Groups @@ -63,6 +63,14 @@ begin dec_trivial end +lemma is_three_cycle.mem_alternating_group {f : perm α} (h : is_three_cycle f) : + f ∈ alternating_group α := +mem_alternating_group.2 h.sign + +lemma fin_rotate_bit1_mem_alternating_group {n : ℕ} : + fin_rotate (bit1 n) ∈ alternating_group (fin (bit1 n)) := +by rw [mem_alternating_group, bit1, sign_fin_rotate, pow_bit0', int.units_mul_self, one_pow] + end equiv.perm lemma two_mul_card_alternating_group [nontrivial α] : @@ -73,9 +81,47 @@ begin exact (subgroup.card_eq_card_quotient_mul_card_subgroup _).symm, end -instance alternating_group_normal : (alternating_group α).normal := sign.normal_ker +namespace alternating_group +open equiv.perm + +instance normal : (alternating_group α).normal := sign.normal_ker + +lemma is_conj_of {σ τ : alternating_group α} + (hc : is_conj (σ : perm α) (τ : perm α)) (hσ : (σ : perm α).support.card + 2 ≤ fintype.card α) : + is_conj σ τ := +begin + obtain ⟨σ, hσ⟩ := σ, + obtain ⟨τ, hτ⟩ := τ, + obtain ⟨π, hπ⟩ := is_conj_iff.1 hc, + rw [subtype.coe_mk, subtype.coe_mk] at hπ, + cases int.units_eq_one_or (sign π) with h h, + { exact is_conj_iff.2 ⟨⟨π, mem_alternating_group.2 h⟩, subtype.val_injective (by simp [← hπ])⟩ }, + { have h2 : 2 ≤ σ.supportᶜ.card, + { rw [finset.card_compl, nat.le_sub_left_iff_add_le σ.support.card_le_univ], + exact hσ }, + obtain ⟨a, ha, b, hb, ab⟩ := finset.one_lt_card.1 h2, + refine is_conj_iff.2 ⟨⟨π * swap a b, _⟩, subtype.val_injective _⟩, + { rw [mem_alternating_group, monoid_hom.map_mul, h, sign_swap ab, int.units_mul_self] }, + { simp only [←hπ, coe_mk, subgroup.coe_mul, subtype.val_eq_coe], + have hd : disjoint (swap a b) σ, + { rw [disjoint_iff_disjoint_support, support_swap ab, finset.disjoint_insert_left, + finset.singleton_disjoint], + exact ⟨finset.mem_compl.1 ha, finset.mem_compl.1 hb⟩ }, + rw [mul_assoc π _ σ, disjoint.mul_comm hd], + simp [mul_assoc] } } +end + +lemma is_three_cycle_is_conj (h5 : 5 ≤ fintype.card α) + {σ τ : alternating_group α} + (hσ : is_three_cycle (σ : perm α)) (hτ : is_three_cycle (τ : perm α)) : + is_conj σ τ := +alternating_group.is_conj_of (is_conj_iff_cycle_type_eq.2 (hσ.trans hτ.symm)) + (by rwa hσ.card_support) + +end alternating_group namespace equiv.perm +open alternating_group @[simp] theorem closure_three_cycles_eq_alternating : @@ -100,4 +146,40 @@ closure_eq_of_le _ (λ σ hσ, mem_alternating_group.2 hσ.sign) $ λ σ hσ, be (ih _ (λ g hg, hl g (list.mem_cons_of_mem _ (list.mem_cons_of_mem _ hg))) hn), end +lemma is_three_cycle.alternating_normal_closure (h5 : 5 ≤ fintype.card α) + {f : perm α} (hf : is_three_cycle f) : + normal_closure ({⟨f, hf.mem_alternating_group⟩} : set (alternating_group α)) = ⊤ := +eq_top_iff.2 begin + have hi : function.injective (alternating_group α).subtype := subtype.coe_injective, + refine eq_top_iff.1 (map_injective hi (le_antisymm (map_mono le_top) _)), + rw [← monoid_hom.range_eq_map, subtype_range, normal_closure, monoid_hom.map_closure], + refine (le_of_eq closure_three_cycles_eq_alternating.symm).trans (closure_mono _), + intros g h, + obtain ⟨c, rfl⟩ := is_conj_iff.1 (is_conj_iff_cycle_type_eq.2 (hf.trans h.symm)), + refine ⟨⟨c * f * c⁻¹, h.mem_alternating_group⟩, _, rfl⟩, + rw group.mem_conjugates_of_set_iff, + exact ⟨⟨f, hf.mem_alternating_group⟩, set.mem_singleton _, is_three_cycle_is_conj h5 hf h⟩ +end + end equiv.perm + +namespace alternating_group +open equiv.perm + +lemma normal_closure_fin_rotate_five : + (normal_closure ({⟨fin_rotate 5, fin_rotate_bit1_mem_alternating_group⟩} : + set (alternating_group (fin 5)))) = ⊤ := +eq_top_iff.2 begin + have h3 : is_three_cycle ((fin.cycle_range 2) * (fin_rotate 5) * + (fin.cycle_range 2)⁻¹ * (fin_rotate 5)⁻¹) := card_support_eq_three_iff.1 dec_trivial, + rw ← h3.alternating_normal_closure (by rw [card_fin]), + refine normal_closure_le_normal _, + rw [set.singleton_subset_iff, set_like.mem_coe], + have h : (⟨fin_rotate 5, fin_rotate_bit1_mem_alternating_group⟩ : + alternating_group (fin 5)) ∈ normal_closure _ := + set_like.mem_coe.1 (subset_normal_closure (set.mem_singleton _)), + exact mul_mem _ (subgroup.normal_closure_normal.conj_mem _ h + ⟨fin.cycle_range 2, fin.is_three_cycle_cycle_range_two.mem_alternating_group⟩) (inv_mem _ h), +end + +end alternating_group diff --git a/src/group_theory/subgroup.lean b/src/group_theory/subgroup.lean index 9f05b8714376c..81bf9ddba6e0f 100644 --- a/src/group_theory/subgroup.lean +++ b/src/group_theory/subgroup.lean @@ -1208,6 +1208,9 @@ lemma range_top_of_surjective {N} [group N] (f : G →* N) (hf : function.surjec f.range = (⊤ : subgroup N) := range_top_iff_surjective.2 hf +@[simp, to_additive] lemma _root_.subgroup.subtype_range (H : subgroup G) : H.subtype.range = H := +by { rw [range_eq_map, ← set_like.coe_set_eq, coe_map, subgroup.coe_subtype], ext, simp } + /-- Restriction of a group hom to a subgroup of the domain. -/ @[to_additive "Restriction of an `add_group` hom to an `add_subgroup` of the domain."] def restrict (f : G →* N) (H : subgroup G) : H →* N := diff --git a/src/linear_algebra/bilinear_form.lean b/src/linear_algebra/bilinear_form.lean index a643f5354a5ed..e44ba37a84128 100644 --- a/src/linear_algebra/bilinear_form.lean +++ b/src/linear_algebra/bilinear_form.lean @@ -790,10 +790,11 @@ by rw [bilin_form.to_matrix, linear_equiv.trans_apply, bilin_form.to_matrix'_app @[simp] lemma matrix.to_bilin_apply (M : matrix n n R₃) (x y : M₃) : matrix.to_bilin hb M x y = ∑ i j, hb.repr x i * M i j * hb.repr y j := -show ((congr hb.equiv_fun).symm (matrix.to_bilin' M)) x y = - ∑ (i j : n), hb.repr x i * M i j * hb.repr y j, -by simp only [congr_symm, congr_apply, linear_equiv.symm_symm, matrix.to_bilin'_apply, - is_basis.equiv_fun_apply] +begin + rw [matrix.to_bilin, bilin_form.to_matrix, linear_equiv.symm_trans_apply, ← matrix.to_bilin'], + simp only [congr_symm, congr_apply, linear_equiv.symm_symm, matrix.to_bilin'_apply, + is_basis.equiv_fun_apply] +end -- Not a `simp` lemma since `bilin_form.to_matrix` needs an extra argument lemma bilinear_form.to_matrix_aux_eq (B : bilin_form R₃ M₃) :