English
For any lift of maps f and g with the specified zero-product and scalar-tensor compatibility, the range of lift is the supremum of the range of f and the algebra generated by the range of g.
Русский
Для произвольного лифта отображений f и g с указанной нулевой продукцией и совместимостью по скалярам, образ лифта равен верхней границе образа f и алгебры, порождаемой образом g.
LaTeX
$$$\\mathrm{range}(\\mathrm{lift}\\ f\\ g\\ hg\\ hfg\\ hgf) = f.\\mathrm{range} \\sqcup Algebra.adjoin\\ S (Set.range g)$$$
Lean4
@[simp]
theorem range_liftAux (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ x y, g x * g y = 0) (hfg : ∀ r x, g (r •> x) = f r * g x)
(hgf : ∀ r x, g (x <• r) = g x * f r) : (lift f g hg hfg hgf).range = f.range ⊔ Algebra.adjoin S (Set.range g) := by
simp_rw [← Algebra.map_top, ← range_inlAlgHom_sup_adjoin_range_inr, Algebra.map_sup, AlgHom.map_adjoin, ←
AlgHom.range_comp, lift_comp_inlHom, ← Set.range_comp, Function.comp_def, lift_apply_inr, Algebra.map_top]
