# Adjoining elements to form subalgebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

theorem algebra.subset_adjoin {R : Type u} {A : Type v} [semiring A] [ A] {s : set A} :
s s)
theorem algebra.adjoin_le {R : Type u} {A : Type v} [semiring A] [ A] {s : set A} {S : A} (H : s S) :
S
theorem algebra.adjoin_eq_Inf {R : Type u} {A : Type v} [semiring A] [ A] {s : set A} :
= has_Inf.Inf {p : A | s p}
theorem algebra.adjoin_le_iff {R : Type u} {A : Type v} [semiring A] [ A] {s : set A} {S : A} :
S s S
theorem algebra.adjoin_mono {R : Type u} {A : Type v} [semiring A] [ A] {s t : set A} (H : s t) :
theorem algebra.adjoin_eq_of_le {R : Type u} {A : Type v} [semiring A] [ A] {s : set A} (S : A) (h₁ : s S) (h₂ : S ) :
= S
theorem algebra.adjoin_eq {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
= S
theorem algebra.adjoin_Union {R : Type u} {A : Type v} [semiring A] [ A] {α : Type u_1} (s : α set A) :
(set.Union s) = (i : α), (s i)
theorem algebra.adjoin_attach_bUnion {R : Type u} {A : Type v} [semiring A] [ A] [decidable_eq A] {α : Type u_1} {s : finset α} (f : s ) :
(s.attach.bUnion f) = (x : s), (f x)
theorem algebra.adjoin_induction {R : Type u} {A : Type v} [semiring A] [ A] {s : set A} {p : A Prop} {x : A} (h : x ) (Hs : (x : A), x s p x) (Halg : (r : R), p ( A) r)) (Hadd : (x y : A), p x p y p (x + y)) (Hmul : (x y : A), p x p y p (x * y)) :
p x
theorem algebra.adjoin_induction₂ {R : Type u} {A : Type v} [semiring A] [ A] {s : set A} {p : A A Prop} {a b : A} (ha : a ) (hb : b ) (Hs : (x : A), x s (y : A), y s p x y) (Halg : (r₁ r₂ : R), p ( A) r₁) ( A) r₂)) (Halg_left : (r : R) (x : A), x s p ( A) r) x) (Halg_right : (r : R) (x : A), x s p x ( A) r)) (Hadd_left : (x₁ x₂ y : A), p x₁ y p x₂ y p (x₁ + x₂) y) (Hadd_right : (x y₁ y₂ : A), p x y₁ p x y₂ p x (y₁ + y₂)) (Hmul_left : (x₁ x₂ y : A), p x₁ y p x₂ y p (x₁ * x₂) y) (Hmul_right : (x y₁ y₂ : A), p x y₁ p x y₂ p x (y₁ * y₂)) :
p a b

Induction principle for the algebra generated by a set s: show that p x y holds for any x y ∈ adjoin R s given that that it holds for x y ∈ s and that it satisfies a number of natural properties.

theorem algebra.adjoin_induction' {R : Type u} {A : Type v} [semiring A] [ A] {s : set A} {p : s) Prop} (Hs : (x : A) (h : x s), p x, _⟩) (Halg : (r : R), p ( s)) r)) (Hadd : (x y : s)), p x p y p (x + y)) (Hmul : (x y : s)), p x p y p (x * y)) (x : 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} [semiring A] [ A] {s : set A} :
theorem algebra.adjoin_union {R : Type u} {A : Type v} [semiring A] [ A] (s t : set A) :
(s t) =
@[simp]
theorem algebra.adjoin_empty (R : Type u) (A : Type v) [semiring A] [ A] :
@[simp]
theorem algebra.adjoin_univ (R : Type u) (A : Type v) [semiring A] [ A] :
theorem algebra.adjoin_eq_span (R : Type u) {A : Type v} [semiring A] [ A] (s : set A) :
theorem algebra.span_le_adjoin (R : Type u) {A : Type v} [semiring A] [ A] (s : set A) :
theorem algebra.adjoin_to_submodule_le (R : Type u) {A : Type v} [semiring A] [ A] {s : set A} {t : A} :
theorem algebra.adjoin_eq_span_of_subset (R : Type u) {A : Type v} [semiring A] [ A] {s : set A} (hs : s)) :
@[simp]
theorem algebra.adjoin_span (R : Type u) {A : Type v} [semiring A] [ A] {s : set A} :
s) =
theorem algebra.adjoin_image (R : Type u) {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (f : A →ₐ[R] B) (s : set A) :
(f '' s) = s)
@[simp]
theorem algebra.adjoin_insert_adjoin (R : Type u) {A : Type v} [semiring A] [ A] (s : set A) (x : A) :
s)) = s)
theorem algebra.adjoin_prod_le (R : Type u) {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (s : set A) (t : set B) :
(s ×ˢ t) s).prod t)
theorem algebra.mem_adjoin_of_map_mul (R : Type u) {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] {s : set A} {x : A} {f : A →ₗ[R] B} (hf : (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂) (h : x ) :
f x (f '' (s {1}))
theorem algebra.adjoin_inl_union_inr_eq_prod (R : Type u) {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (s : set A) (t : set B) :
( A B) '' (s {1}) A B) '' (t {1})) = s).prod t)
def algebra.adjoin_comm_semiring_of_comm (R : Type u) {A : Type v} [semiring A] [ A] {s : set A} (hcomm : (a : A), a s (b : A), b s a * b = b * a) :

If all elements of s : set A commute pairwise, then adjoin R s is a commutative semiring.

Equations
theorem algebra.adjoin_singleton_one (R : Type u) {A : Type v} [semiring A] [ A] :
{1} =
theorem algebra.self_mem_adjoin_singleton (R : Type u) {A : Type v} [semiring A] [ A] (x : A) :
x {x}
theorem algebra.adjoin_union_eq_adjoin_adjoin (R : Type u) {A : Type v} [ A] (s t : set A) :
(s t) =
theorem algebra.adjoin_union_coe_submodule (R : Type u) {A : Type v} [ A] (s t : set A) :
theorem algebra.adjoin_adjoin_of_tower (R : Type u) {A : Type v} {B : Type w} [ A] [semiring B] [ B] [ B] [ B] (s : set B) :
s) =
theorem algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin {R : Type u} {A : Type v} {B : Type w} [ A] [ B] [ B] [ B] (r : A) (s : set B) (B' : B) (hs : r s B') {x : B} (hx : x ) (hr : B) r B') :
(n₀ : ), (n : ), n n₀ r ^ n x B'
theorem algebra.pow_smul_mem_adjoin_smul {R : Type u} {A : Type v} [ A] (r : R) (s : set A) {x : A} (hx : x ) :
(n₀ : ), (n : ), n n₀ r ^ n x (r s)
theorem algebra.adjoin_int {R : Type u} [comm_ring R] (s : set R) :
theorem algebra.mem_adjoin_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] {s : set A} {x : A} :
theorem algebra.adjoin_eq_ring_closure {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] (s : set A) :
def algebra.adjoin_comm_ring_of_comm (R : Type u) {A : Type v} [comm_ring R] [ring A] [ A] {s : set A} (hcomm : (a : A), a s (b : A), b s a * b = b * a) :

If all elements of s : set A commute pairwise, then adjoin R s is a commutative ring.

Equations
theorem alg_hom.map_adjoin {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (φ : A →ₐ[R] B) (s : set A) :
s) = (φ '' s)
theorem alg_hom.adjoin_le_equalizer {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (φ₁ φ₂ : A →ₐ[R] B) {s : set A} (h : φ₂ s) :
φ₁.equalizer φ₂
theorem alg_hom.ext_of_adjoin_eq_top {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] {s : set A} (h : = ) ⦃φ₁ φ₂ : A →ₐ[R] B⦄ (hs : φ₂ s) :
φ₁ = φ₂