feat(ring_theory/adjoin/basic): add adjoin_induction' and adjoin_adjo…

…in_coe_preimage (#10427)

From FLT-regular.
Co-authored-by: Chris Birkbeck <cd.birkbeck@gmail.com>

src/group_theory/subgroup/basic.lean

@@ -653,6 +653,17 @@ subtype.rec_on x $ λ x hx, begin
     (λ x hx, exists.elim hx $ λ hx' hx, ⟨inv_mem _ hx', Hinv _ hx⟩),
 end
 
+@[simp, to_additive]
+lemma closure_closure_coe_preimage {k : set G} : closure ((coe : closure k → G) ⁻¹' k) = ⊤ :=
+begin
+  refine eq_top_iff.2 (λ x hx, closure_induction' (λ x, _) _ _ (λ g₁ g₂ hg₁ hg₂, _) (λ g hg, _) x),
+  { intros g hg,
+    exact subset_closure hg },
+  { exact subgroup.one_mem _ },
+  { exact subgroup.mul_mem _ hg₁ hg₂ },
+  { exact subgroup.inv_mem _ hg }
+end
+
 variable (G)
 
 /-- `closure` forms a Galois insertion with the coercion to set. -/

src/group_theory/submonoid/operations.lean

@@ -488,6 +488,16 @@ subtype.rec_on x $ λ x hx, begin
       ⟨mul_mem _ hx' hy', Hmul _ _ hx hy⟩),
 end
 
+@[simp, to_additive]
+lemma closure_closure_coe_preimage {s : set M} : closure ((coe : closure s → M) ⁻¹' s) = ⊤ :=
+begin
+  refine eq_top_iff.2 (λ x hx, closure_induction' (λ x, _) _ _ (λ g₁ g₂ hg₁ hg₂, _) x),
+  { intros g hg,
+    exact subset_closure hg },
+  { exact submonoid.one_mem _ },
+  { exact submonoid.mul_mem _ hg₁ hg₂ },
+end
+
 /-- Given `submonoid`s `s`, `t` of monoids `M`, `N` respectively, `s × t` as a submonoid
 of `M × N`. -/
 @[to_additive prod "Given `add_submonoid`s `s`, `t` of `add_monoid`s `A`, `B` respectively, `s × t`

src/linear_algebra/basic.lean

@@ -863,6 +863,27 @@ preserved under addition and scalar multiplication, then `p` holds for all eleme
   (H2 : ∀ (a:R) x, p x → p (a • x)) : p x :=
 (@span_le _ _ _ _ _ _ ⟨p, H0, H1, H2⟩).2 Hs h
 
+/-- The difference with `submodule.span_induction` is that this acts on the subtype. -/
+lemma span_induction' {p : span R s → Prop} (Hs : ∀ x (h : x ∈ s), p ⟨x, subset_span h⟩) (H0 : p 0)
+  (H1 : ∀ x y, p x → p y → p (x + y)) (H2 : ∀ (a : R) x, p x → p (a • x)) (x : span R s) : p x :=
+subtype.rec_on x $ λ x hx, begin
+  refine exists.elim _ (λ (hx : x ∈ span R s) (hc : p ⟨x, hx⟩), hc),
+  refine span_induction hx (λ m hm, ⟨subset_span hm, Hs m hm⟩) ⟨zero_mem _, H0⟩
+    (λ x y hx hy, exists.elim hx $ λ hx' hx, exists.elim hy $ λ hy' hy,
+    ⟨add_mem _ hx' hy', H1 _ _ hx hy⟩) (λ r x hx, exists.elim hx $ λ hx' hx,
+    ⟨smul_mem _ _ hx', H2 r _ hx⟩)
+end
+
+@[simp] lemma span_span_coe_preimage : span R ((coe : span R s → M) ⁻¹' s) = ⊤ :=
+begin
+  refine eq_top_iff.2 (λ x hx, span_induction' (λ x hx, _) _ _ (λ r x hx, _) x),
+  { exact subset_span hx },
+  { exact submodule.zero_mem _ },
+  { intros x y hx hy,
+    exact submodule.add_mem _ hx hy },
+  { exact submodule.smul_mem _ _ hx }
+end
+
 lemma span_nat_eq_add_submonoid_closure (s : set M) :
   (span ℕ s).to_add_submonoid = add_submonoid.closure s :=
 begin

src/ring_theory/adjoin/basic.lean

@@ -64,6 +64,29 @@ let S : subalgebra R A :=
 { carrier := p, mul_mem' := Hmul, add_mem' := Hadd, algebra_map_mem' := Halg } in
 adjoin_le (show s ≤ S, from Hs) h
 
+/-- The difference with `algebra.adjoin_induction` is that this acts on the subtype. -/
+lemma adjoin_induction' {p : adjoin R s → Prop} (Hs : ∀ x (h : x ∈ s), p ⟨x, subset_adjoin h⟩)
+  (Halg : ∀ r, p (algebra_map R _ r)) (Hadd : ∀ x y, p x → p y → p (x + y))
+  (Hmul : ∀ x y, p x → p y → p (x * y)) (x : adjoin R s) : p x :=
+subtype.rec_on x $ λ x hx, begin
+  refine exists.elim _ (λ (hx : x ∈ adjoin R s) (hc : p ⟨x, hx⟩), hc),
+  exact adjoin_induction hx (λ x hx, ⟨subset_adjoin hx, Hs x hx⟩)
+    (λ r, ⟨subalgebra.algebra_map_mem _ r, Halg r⟩)
+    (λ x y hx hy, exists.elim hx $ λ hx' hx, exists.elim hy $ λ hy' hy,
+    ⟨subalgebra.add_mem _ hx' hy', Hadd _ _ hx hy⟩) (λ x y hx hy, exists.elim hx $ λ hx' hx,
+    exists.elim hy $ λ hy' hy, ⟨subalgebra.mul_mem _ hx' hy', Hmul _ _ hx hy⟩),
+end
+
+@[simp] lemma adjoin_adjoin_coe_preimage {s : set A} :
+  adjoin R ((coe : adjoin R s → A) ⁻¹' s) = ⊤ :=
+begin
+  refine eq_top_iff.2 (λ x, adjoin_induction' (λ a ha, _) (λ r, _) (λ _ _, _) (λ _ _, _) x),
+  { exact subset_adjoin ha },
+  { exact subalgebra.algebra_map_mem _ r },
+  { exact subalgebra.add_mem _ },
+  { exact subalgebra.mul_mem _ }
+end
+
 lemma adjoin_union (s t : set A) : adjoin R (s ∪ t) = adjoin R s ⊔ adjoin R t :=
 (algebra.gc : galois_connection _ (coe : subalgebra R A → set A)).l_sup