English
The range of liftHom equals the algebra generated by the images of i, j, k, i.e., the subalgebra generated by {i, j, k} inside A.
Русский
Образ liftHom равен подалгебре внутри A, порождённой изображениями i, j, k.
LaTeX
$$(liftHom).range = \\mathrm{Alg\\!-\!adjoin}\\, R\\{ q.i, q.j, q.k \\}$$
Lean4
@[simp]
theorem range_liftHom (B : Basis A c₁ c₂ c₃) : (liftHom B).range = Algebra.adjoin R { B.i, B.j, B.k } :=
by
apply le_antisymm
· rintro x ⟨y, rfl⟩
refine add_mem (add_mem (add_mem ?_ ?_) ?_) ?_
· exact algebraMap_mem _ _
all_goals exact Subalgebra.smul_mem _ (Algebra.subset_adjoin <| by simp) _
· rw [Algebra.adjoin_le_iff]
rintro x (rfl | rfl | rfl) <;> [use (Basis.self R).i; use (Basis.self R).j; use (Basis.self R).k]
all_goals simp [lift]
