isHomLift_homCartesianLift — Mathlib

English

If φ′ is a lift of g ∘ f, then the morphism homCartesianLift(f,g,φ′) is itself a lift of g with respect to the forgetful functor; i.e., it satisfies the IsHomLift property for g.

Русский

Если φ′ является подъемом над g ∘ f, то отображение homCartesianLift(f,g,φ′) само по себе является подъемом над g относительно забывающего функторa; то есть удовлетворяет свойству IsHomLift для g.

LaTeX

$$$\\text{IsHomLift}(\\mathrm{forget}\ F)(g, \\mathrm{homCartesianLift}(f,g,\\phi'))$$$

Lean4

instance isHomLift_homCartesianLift {a' : ∫ᶜ F} {φ' : a' ⟶ ⟨S, a⟩} {g : a'.1 ⟶ R} [IsHomLift (forget F) (g ≫ f) φ'] :
    IsHomLift (forget F) g (homCartesianLift f g φ') :=
  IsHomLift.map (forget F) (homCartesianLift f g φ')

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