More operations on subalgebras

In this file we relate the definitions in Mathlib.RingTheory.Ideal.Operations to subalgebras. The contents of this file are somewhat random since both Mathlib.Algebra.Algebra.Subalgebra.Basic and Mathlib.RingTheory.Ideal.Operations are somewhat of a grab-bag of definitions, and this is whatever ends up in the intersection.

theorem AlgHom.ker_rangeRestrict {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) : RingHom.ker f.rangeRestrict = RingHom.ker f

theorem Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommRing S] [Algebra R S] (S' : Subalgebra R S) {ι : Type u_3} (ι' : Finset ι) (s : ι → S) (l : ι → S) (e : (ι'.sum fun (i : ι) => l i * s i) = 1) (hs : ∀ (i : ι), s i ∈ S') (hl : ∀ (i : ι), l i ∈ S') (x : S) (H : ∀ (i : ι), ∃ (n : ℕ), s i ^ n • x ∈ S') : x ∈ S'

Suppose we are given ∑ i, lᵢ * sᵢ = 1 in S, and S' a subalgebra of S that contains lᵢ and sᵢ. To check that an x : S falls in S', we only need to show that sᵢ ^ n • x ∈ S' for some n for each sᵢ.

theorem Subalgebra.mem_of_span_eq_top_of_smul_pow_mem {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommRing S] [Algebra R S] (S' : Subalgebra R S) (s : Set S) (l : ↑s →₀ S) (hs : (Finsupp.total (↑s) S S Subtype.val) l = 1) (hs' : s ⊆ ↑S') (hl : ∀ (i : ↑s), l i ∈ S') (x : S) (H : ∀ (r : ↑s), ∃ (n : ℕ), ↑r ^ n • x ∈ S') : x ∈ S'