iSupLift_comp_inclusion — Mathlib

English

Under the same setup as above, the lifted map composed with the inclusion equals the corresponding f_i. Precisely, for each i and each h with K_i ≤ T, we have (iSupLift K dir f hf T hT) ∘ inclusion h = f_i.

Русский

В той же конфигурации, что выше, подъём, сочетающийся с включением, равен соответствующему f_i. Точно: для каждого i выполнено (iSupLift K dir f hf T hT) ∘ inclusion h = f_i.

LaTeX

$$$ (iSupLift K dir f hf T hT) \circ (inclusion\ h) = f_i $$$

Lean4

@[simp]
theorem iSupLift_comp_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 : ι}
    (h : K i ≤ T) : (iSupLift K dir f hf T hT).comp (inclusion h) = f i := by ext; simp

Похожие утверждения