lift — Mathlib

English

If the image of f lies in G, then f factors through G.

Русский

Если образ f лежит в G, то существует факторизация f через G.

LaTeX

$$range f ≤ G → ∃ l : F' ⟶ G.toPresheaf, ∀ U x, l.app U x = ⟨f.app U x, hf U _⟩$$

Lean4

/-- If the image of a morphism falls in a subpresheaf, then the morphism factors through it. -/
@[simps!]
def lift : F' ⟶ G.toPresheaf where
  app U x := ⟨f.app U x, hf U (by simp)⟩
  naturality _ _
    g := by
    ext x
    simpa [Subtype.ext_iff] using FunctorToTypes.naturality _ _ f g x

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