English
Let (K_i) be a directed family of subalgebras of A over R, and suppose f_i: K_i → B are algebra homomorphisms that are compatible with inclusions, i.e. f_i = f_j ∘ inclusion whenever K_i ≤ K_j. Let T = iSup K and hT : T = iSup K. Then for every i, every x ∈ K_i with K_i ≤ T, the lifted map iSupLift K dir f hf T hT evaluated at inclusion h applied to x equals f_i(x). In other words, the lift agrees with each f_i on the corresponding component of the directed system.
Русский
Пусть (K_i) задаёт направленный семейство подполь подалгебр A над R, и пусть f_i: K_i → B — алгебра морфизмы, совместимые по включениям, то есть f_i = f_j ∘ включение, когда K_i ≤ K_j. Обозначим T = iSup K и hT: T = iSup K. Тогда для любого i и любого x ∈ K_i с условием K_i ≤ T верно: iSupLift K dir f hf T hT (inclusion h x) = f_i(x). Иными словами, подъём согласуется с каждым f_i на соответствующем элементе противостоящей системы.
LaTeX
$$$\forall i\in I,\forall x\in K_i,\ K_i \le T \ \Rightarrow\ iSupLift K dir f hf T hT (\mathrm{inclusion}\; h\; x) = f_i(x)$$$
Lean4
@[simp]
theorem iSupLift_inclusion {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
{hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)} {T : Subalgebra R A} {hT : T = iSup K} {i : ι}
(x : K i) (h : K i ≤ T) : iSupLift K dir f hf T hT (inclusion h x) = f i x :=
by
dsimp [iSupLift, inclusion]
rw [Set.iUnionLift_inclusion]
