functorInclusion_is_mono — Mathlib

English

If for each i a family p₁ i, p₂ i forms a pullback with g and f i, then Sieve.ofArrows P p₁ equals the pullback of g with Sieve.ofArrows X f.

Русский

Если для каждого i семейство p₁ i, p₂ i образуют точный pullback с g и f i, то Sieve.ofArrows P p₁ равна pullback g над Sieve.ofArrows X f.

LaTeX

$$$\\text{Sieve.ofArrows } P p₁ = \\text{Sieve.pullback } g (\\text{Sieve.ofArrows } X f)$$$

Lean4

/-- The presheaf induced by a sieve is a subobject of the yoneda embedding. -/
instance functorInclusion_is_mono : Mono S.functorInclusion :=
  ⟨fun f g h => by
    ext Y y
    simpa [Subtype.ext_iff] using congr_fun (NatTrans.congr_app h Y) y⟩
    -- TODO: Show that when `f` is mono, this is right inverse to `functorInclusion` up to isomorphism.

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