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
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 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')
:
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]
[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')
:
def
FixedPoints.subring
(B : Type u_2)
[CommRing B]
(G : Type u_3)
[Monoid G]
[MulSemiringAction G B]
:
Subring B
The set of fixed points under a group action, as a subring.
Equations
Instances For
def
FixedPoints.subalgebra
(A : Type u_1)
(B : Type u_2)
[CommRing A]
[CommRing B]
[Algebra A B]
(G : Type u_3)
[Monoid G]
[MulSemiringAction G B]
[SMulCommClass G A B]
:
Subalgebra A B
The set of fixed points under a group action, as a subalgebra.