More operations on subalgebras

In this file we relate the definitions in Mathlib/RingTheory/Ideal/Operations.lean to subalgebras. The contents of this file are somewhat random since both Mathlib/Algebra/Algebra/Subalgebra/Basic.lean and Mathlib/RingTheory/Ideal/Operations.lean 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_finsetSum_eq_one_of_pow_smul_mem {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (S' : Subalgebra R S) {ι : Type u_3} (ι' : Finset ι) (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ᵢ = 1 ∈ 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ᵢ.

@[deprecated Subalgebra.mem_of_finsetSum_eq_one_of_pow_smul_mem (since := "2026-04-08")]

theorem Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (S' : Subalgebra R S) {ι : Type u_3} (ι' : Finset ι) (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'

Alias of Subalgebra.mem_of_finsetSum_eq_one_of_pow_smul_mem.

---

Suppose we are given ∑ i, lᵢ * sᵢ = 1 ∈ 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] [CommSemiring 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'

def FixedPoints.subsemiring (B' : Type u_3) [Semiring B'] (G : Type u_4) [Monoid G] [MulSemiringAction G B'] : Subsemiring B'

The set of fixed points under a group action, as a subring.

Equations

• FixedPoints.subsemiring B' G = { carrier := (FixedPoints.addSubmonoid G B').carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

def FixedPoints.subring (B : Type u_2) [Ring B] (G : Type u_4) [Monoid G] [MulSemiringAction G B] : Subring B

The set of fixed points under a group action, as a subring.

Equations

• FixedPoints.subring B G = { carrier := (B^+G).carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

def FixedPoints.subalgebra (A : Type u_1) (B' : Type u_3) [CommSemiring A] [Semiring B'] [Algebra A B'] (G : Type u_4) [Monoid G] [MulSemiringAction G B'] [SMulCommClass G A B'] : Subalgebra A B'

The set of fixed points under a group action, as a subalgebra.

Equations

• FixedPoints.subalgebra A B' G = { toSubsemiring := FixedPoints.subsemiring B' G, algebraMap_mem' := ⋯ }