mathlib documentation

ring_theory.adjoin.basic

Adjoining elements to form subalgebras #

This file develops the basic theory of subalgebras of an R-algebra generated by a set of elements. A basic interface for adjoin is set up.

Tags #

adjoin, algebra

theorem algebra.subset_adjoin {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} :
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} (H : s S) :
theorem algebra.adjoin_eq_Inf {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} :
algebra.adjoin R s = Inf {p : subalgebra R A | s p}
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} :
theorem algebra.adjoin_mono {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s t : set A} (H : s t) :
theorem algebra.adjoin_eq_of_le {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} (S : subalgebra R A) (h₁ : s S) (h₂ : S algebra.adjoin R s) :
theorem algebra.adjoin_eq {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
theorem algebra.adjoin_Union {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {α : Type u_1} (s : α → set A) :
algebra.adjoin R (set.Union s) = ⨆ (i : α), algebra.adjoin R (s i)
theorem algebra.adjoin_attach_bUnion {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] [decidable_eq A] {α : Type u_1} {s : finset α} (f : s → finset A) :
theorem algebra.adjoin_induction {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} {p : A → Prop} {x : A} (h : x algebra.adjoin R s) (Hs : ∀ (x : A), x sp x) (Halg : ∀ (r : R), p ((algebra_map R A) r)) (Hadd : ∀ (x y : A), p xp yp (x + y)) (Hmul : ∀ (x y : A), p xp yp (x * y)) :
p x
theorem algebra.adjoin_induction' {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} {p : (algebra.adjoin R s) → Prop} (Hs : ∀ (x : A) (h : x s), p x, _⟩) (Halg : ∀ (r : R), p ((algebra_map R (algebra.adjoin R s)) r)) (Hadd : ∀ (x y : (algebra.adjoin R s)), p xp yp (x + y)) (Hmul : ∀ (x y : (algebra.adjoin R s)), p xp yp (x * y)) (x : (algebra.adjoin R s)) :
p x

The difference with algebra.adjoin_induction is that this acts on the subtype.

@[simp]
theorem algebra.adjoin_adjoin_coe_preimage {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} :
theorem algebra.adjoin_union {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s t : set A) :
@[simp]
theorem algebra.adjoin_empty (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
@[simp]
theorem algebra.adjoin_univ (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
theorem algebra.adjoin_eq_span (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s : set A) :
theorem algebra.span_le_adjoin (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s : set A) :
theorem algebra.adjoin_to_submodule_le (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} {t : submodule R A} :
theorem algebra.adjoin_eq_span_of_subset (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} (hs : (submonoid.closure s) (submodule.span R s)) :
theorem algebra.adjoin_image (R : Type u) {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (s : set A) :
@[simp]
theorem algebra.adjoin_insert_adjoin (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s : set A) (x : A) :
theorem algebra.adjoin_prod_le (R : Type u) {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (s : set A) (t : set B) :
theorem algebra.mem_adjoin_of_map_mul (R : Type u) {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {s : set A} {x : A} {f : A →ₗ[R] B} (hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = (f a₁) * f a₂) (h : x algebra.adjoin R s) :
f x algebra.adjoin R (f '' (s {1}))
theorem algebra.adjoin_inl_union_inr_eq_prod (R : Type u) {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (s : set A) (t : set B) :
theorem algebra.adjoin_singleton_one (R : Type u) {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] :
theorem algebra.pow_smul_mem_adjoin_smul (R : Type u) {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] (r : R) (s : set A) {x : A} (hx : x algebra.adjoin R s) :
∃ (n₀ : ), ∀ (n : ), n n₀r ^ n x algebra.adjoin R (r s)
theorem algebra.mem_adjoin_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {s : set A} {x : A} :
theorem algebra.adjoin_eq_ring_closure {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (s : set A) :
theorem alg_hom.map_adjoin {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (s : set A) :
theorem alg_hom.adjoin_le_equalizer {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ₁ φ₂ : A →ₐ[R] B) {s : set A} (h : set.eq_on φ₁ φ₂ s) :
algebra.adjoin R s φ₁.equalizer φ₂
theorem alg_hom.ext_of_adjoin_eq_top {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {s : set A} (h : algebra.adjoin R s = ) ⦃φ₁ φ₂ : A →ₐ[R] B⦄ (hs : set.eq_on φ₁ φ₂ s) :
φ₁ = φ₂