English
The adjoin construction adjoin R s yields the smallest nonunital subalgebra of A containing the set s.
Русский
Пусть s ⊆ A; образующая подалгебра adjoin R s является наименьшей неполной подпалгеброй A, содержащей s.
LaTeX
$$$\operatorname{adjoin}_R(s) = \text{the smallest NonUnitalSubalgebra }(A) \text{ containing } s$$$
Lean4
/-- The minimal non-unital subalgebra that includes `s`. -/
def adjoin (s : Set A) : NonUnitalSubalgebra R A :=
{ Submodule.span R (NonUnitalSubsemiring.closure s : Set A) with
mul_mem' :=
fun {a b} (ha : a ∈ Submodule.span R (NonUnitalSubsemiring.closure s : Set A))
(hb : b ∈ Submodule.span R (NonUnitalSubsemiring.closure s : Set A)) =>
show a * b ∈ Submodule.span R (NonUnitalSubsemiring.closure s : Set A)
by
refine Submodule.span_induction ?_ ?_ ?_ ?_ ha
· refine Submodule.span_induction ?_ ?_ ?_ ?_ hb
·
exact fun x (hx : x ∈ NonUnitalSubsemiring.closure s) y (hy : y ∈ NonUnitalSubsemiring.closure s) =>
Submodule.subset_span (mul_mem hy hx)
· exact fun x _hx => (mul_zero x).symm ▸ Submodule.zero_mem _
· exact fun x y _ _ hx hy z hz => (mul_add z x y).symm ▸ add_mem (hx z hz) (hy z hz)
· exact fun r x _ hx y hy => (mul_smul_comm r y x).symm ▸ SMulMemClass.smul_mem r (hx y hy)
· exact (zero_mul b).symm ▸ Submodule.zero_mem _
· exact fun x y _ _ => (add_mul x y b).symm ▸ add_mem
· exact fun r x _ hx => (smul_mul_assoc r x b).symm ▸ SMulMemClass.smul_mem r hx }
