Documentation

Mathlib.Algebra.Algebra.Subalgebra.Operations

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 : 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ᵢ = 1S, 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.linearCombination 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'