From a6158f1988a622da8b4568854f4680bada36c9ee Mon Sep 17 00:00:00 2001 From: tb65536 Date: Thu, 17 Mar 2022 11:06:28 +0000 Subject: [PATCH] feat(group_theory/subgroup/basic): One-sided closure induction lemmas (#12725) This PR adds one-sided closure induction lemmas, which I will need for Schreier's lemma. Co-authored-by: tb65536 --- src/group_theory/subgroup/basic.lean | 23 +++++++++++++--------- src/group_theory/submonoid/membership.lean | 18 +++++++++++++++++ 2 files changed, 32 insertions(+), 9 deletions(-) diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean index 984eadc8b167e..df4476a956948 100644 --- a/src/group_theory/subgroup/basic.lean +++ b/src/group_theory/subgroup/basic.lean @@ -834,6 +834,18 @@ begin { simp only [true_and, coe_to_submonoid, union_subset_iff, subset_closure, inv_subset_closure] } end +@[to_additive] lemma closure_induction_left {p : G → Prop} {x : G} + (h : x ∈ closure k) (H1 : p 1) (Hmul : ∀ (x ∈ k) y, p y → p (x * y)) + (Hinv : ∀ (x ∈ k) y, p y → p (x⁻¹ * y)) : p x := +let key := le_of_eq (closure_to_submonoid k) in submonoid.closure_induction_left (key h) H1 + (λ x hx, hx.elim (Hmul x) (λ hx y hy, (congr_arg _ (inv_inv x)).mp (Hinv x⁻¹ hx y hy))) + +@[to_additive] lemma closure_induction_right {p : G → Prop} {x : G} + (h : x ∈ closure k) (H1 : p 1) (Hmul : ∀ x (y ∈ k), p x → p (x * y)) + (Hinv : ∀ x (y ∈ k), p x → p (x * y⁻¹)) : p x := +let key := le_of_eq (closure_to_submonoid k) in submonoid.closure_induction_right (key h) H1 + (λ x y hy, hy.elim (Hmul x y) (λ hy hx, (congr_arg _ (inv_inv y)).mp (Hinv x y⁻¹ hy hx))) + /-- An induction principle for closure membership. If `p` holds for `1` and all elements of `k` and their inverse, and is preserved under multiplication, then `p` holds for all elements of the closure of `k`. -/ @@ -843,15 +855,8 @@ elements of the additive closure of `k`."] lemma closure_induction'' {p : G → Prop} {x} (h : x ∈ closure k) (Hk : ∀ x ∈ k, p x) (Hk_inv : ∀ x ∈ k, p x⁻¹) (H1 : p 1) (Hmul : ∀ x y, p x → p y → p (x * y)) : p x := -begin - rw [← mem_to_submonoid, closure_to_submonoid k] at h, - refine submonoid.closure_induction h (λ x hx, _) H1 (λ x y hx hy, Hmul x y hx hy), - { rw [mem_union, mem_inv] at hx, - cases hx with mem invmem, - { exact Hk x mem }, - { rw [← inv_inv x], - exact Hk_inv _ invmem } }, -end +closure_induction_left h H1 (λ x hx y hy, Hmul x y (Hk x hx) hy) + (λ x hx y hy, Hmul x⁻¹ y (Hk_inv x hx) hy) /-- An induction principle for elements of `⨆ i, S i`. If `C` holds for `1` and all elements of `S i` for all `i`, and is preserved under multiplication, diff --git a/src/group_theory/submonoid/membership.lean b/src/group_theory/submonoid/membership.lean index 7a4afcc18b3d9..77a4106f9a13a 100644 --- a/src/group_theory/submonoid/membership.lean +++ b/src/group_theory/submonoid/membership.lean @@ -253,6 +253,24 @@ begin exact ⟨l, h1, (multiset.coe_prod l).trans h2⟩, end +@[to_additive] +lemma closure_induction_left {s : set M} {p : M → Prop} {x : M} (h : x ∈ closure s) (H1 : p 1) + (Hmul : ∀ (x ∈ s) y, p y → p (x * y)) : p x := +begin + rw closure_eq_mrange at h, + obtain ⟨l, rfl⟩ := h, + induction l using free_monoid.rec_on with x y ih, + { exact H1 }, + { simpa only [map_mul, free_monoid.lift_eval_of] using Hmul _ x.prop _ ih } +end + +@[to_additive] +lemma closure_induction_right {s : set M} {p : M → Prop} {x : M} (h : x ∈ closure s) (H1 : p 1) + (Hmul : ∀ x (y ∈ s), p x → p (x * y)) : p x := +@closure_induction_left _ _ (mul_opposite.unop ⁻¹' s) (p ∘ mul_opposite.unop) (mul_opposite.op x) + (closure_induction h (λ x hx, subset_closure hx) (one_mem _) (λ x y hx hy, mul_mem _ hy hx)) + H1 (λ x hx y, Hmul _ _ hx) + /-- The submonoid generated by an element. -/ def powers (n : M) : submonoid M := submonoid.copy (powers_hom M n).mrange (set.range ((^) n : ℕ → M)) $