instIsFiberedForget — Mathlib

English

The forgetful functor forget F from the Grothendieck construction ∫ᶜ F to the base category 𝒮 is fibered; equivalently, every morphism in 𝒮 has Cartesian lifts with respect to forget F.

Русский

Забывающий функтор forget F из конструкций Гротендика ∫ᶜ F в основанную категорию 𝒮 является фиберованной; эквивалентно, каждый морфизм в 𝒮 имеет картезианские подъёмы относительно forget F.

LaTeX

$$$\\text{forget }F \\text{ is fibered over } 𝒮$$$

Lean4

/-- `forget F : ∫ᶜ F ⥤ 𝒮` is a fibered category. -/
instance : IsFibered (forget F) :=
  IsFibered.of_exists_isStronglyCartesian
    (fun a _ f ↦ ⟨domainCartesianLift a.2 f, cartesianLift a.2 f, isStronglyCartesian_homCartesianLift a.2 f⟩)

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