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

@@ -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

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)

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
 
 /-!

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

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

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]

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

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 :=

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₃) :