lift — Mathlib

English

Compatibility of lift with projections in the is-sheaf equivalence framework.

Русский

Совместимость подъема с проекциями в системе эквивалентности is-sheaf.

LaTeX

$$$ fac'\\ (i) : lift\\ hP\\ hE le F \\;\\Rightarrow\\; F.ι ⟨_, E.f i, le _ (Sieve.ofArrows_mk _ _ _)\\rangle$$$

Lean4

/-- Auxiliary definition for `isLimit`. -/
noncomputable def lift : F.pt ⟶ P.obj (Opposite.op X) :=
  Multifork.IsLimit.lift (hP E hE).some (fun i => F.ι ⟨_, E.f i, le _ (Sieve.ofArrows_mk _ _ _)⟩)
    (fun ⟨⟨i₁, i₂⟩, j⟩ =>
      F.condition
        { fst := { hf := le _ (Sieve.ofArrows_mk _ _ i₁), .. }
          snd := { hf := le _ (Sieve.ofArrows_mk _ _ i₂), .. }
          r := { w := E.w j, .. } })

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