lift_comp — Mathlib

English

For every g and h satisfying the invertibility condition, there exists a unique l with l ∘ f = g.

Русский

Для каждого g и h, удовлетворяющих условию инвертируемости, существует единственный l с l ∘ f = g.

LaTeX

$$$$ \forall g, \forall h, \exists! l : M' \to M'': l \circ f = g. $$$$

Lean4

theorem lift_comp (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)) :
    (lift S f g h).comp f = g := by
  dsimp only [IsLocalizedModule.lift]
  rw [LinearMap.comp_assoc, iso_symm_comp, LocalizedModule.lift_comp S g h]

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