theorem
algebra.subset_adjoin
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s : set A} :
s ⊆ ↑(algebra.adjoin R s)
theorem
algebra.adjoin_le
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s : set A}
{S : subalgebra R A} :
s ⊆ ↑S → algebra.adjoin R s ≤ S
theorem
algebra.adjoin_le_iff
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s : set A}
{S : subalgebra R A} :
algebra.adjoin R s ≤ S ↔ s ⊆ ↑S
theorem
algebra.adjoin_mono
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s t : set A} :
s ⊆ t → algebra.adjoin R s ≤ algebra.adjoin R t
@[simp]
theorem
algebra.adjoin_empty
(R : Type u)
(A : Type v)
[comm_semiring R]
[semiring A]
[algebra R A] :
algebra.adjoin R ∅ = ⊥
theorem
algebra.adjoin_eq_span
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(s : set A) :
↑(algebra.adjoin R s) = submodule.span R (monoid.closure s)
theorem
algebra.adjoin_union
(R : Type u)
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(s t : set A) :
algebra.adjoin R (s ∪ t) = (algebra.adjoin R s).under (algebra.adjoin ↥(algebra.adjoin R s) t)
theorem
algebra.adjoin_eq_range
(R : Type u)
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(s : set A) :
theorem
algebra.adjoin_singleton_eq_range
(R : Type u)
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(x : A) :
algebra.adjoin R {x} = (polynomial.aeval x).range
theorem
algebra.adjoin_union_coe_submodule
(R : Type u)
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(s t : set A) :
↑(algebra.adjoin R (s ∪ t)) = ↑(algebra.adjoin R s) * ↑(algebra.adjoin R t)
theorem
algebra.mem_adjoin_iff
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
{s : set A}
{x : A} :
x ∈ algebra.adjoin R s ↔ x ∈ ring.closure (set.range ⇑(algebra_map R A) ∪ s)
theorem
algebra.adjoin_eq_ring_closure
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
(s : set A) :
↑(algebra.adjoin R s) = ring.closure (set.range ⇑(algebra_map R A) ∪ s)
theorem
algebra.fg_trans
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
{s t : set A} :
↑(algebra.adjoin R s).fg → ↑(algebra.adjoin ↥(algebra.adjoin R s) t).fg → ↑(algebra.adjoin R (s ∪ t)).fg
def
subalgebra.fg
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A] :
subalgebra R A → Prop
A subalgebra S is finitely generated if there exists t : finset A such that
algebra.adjoin R t = S.
theorem
subalgebra.fg_def
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
{S : subalgebra R A} :
@[instance]
def
alg_hom.is_noetherian_ring_range
{R : Type u}
{A : Type v}
{B : Type w}
[comm_ring R]
[comm_ring A]
[comm_ring B]
[algebra R A]
[algebra R B]
(f : A →ₐ[R] B)
[is_noetherian_ring A] :
Equations
- _ = _
theorem
is_noetherian_ring_of_fg
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
{S : subalgebra R A}
(HS : S.fg)
[is_noetherian_ring R] :
theorem
is_noetherian_ring_closure
{R : Type u}
[comm_ring R]
(s : set R) :
s.finite → is_noetherian_ring ↥(ring.closure s)