lift_injective — Mathlib

English

If e is an equivalence of component systems compatible with f, then applying e to a representative preserves the direct limit identifications.

Русский

Если e — эквивалентность компонентной системы, согласованная с f, то применение e к представителю сохраняет идентификации пределa.

LaTeX

$$$\operatorname{congr}(e,he)(\text{of}(i,g)) = \text{of}(i, e_i(g))$$$

Lean4

theorem lift_injective [IsDirected ι (· ≤ ·)] (injective : ∀ i, Function.Injective <| g i) :
    Function.Injective (lift G f P g Hg) :=
  Module.DirectLimit.lift_injective (f := fun i j hij ↦ (f i j hij).toNatLinearMap) _ Hg injective

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