instPreservesFiniteProductsOppositeTopCatYonedaPresheaf'

English

The universe-polymorphic Yoneda presheaf preserves finite products.

Русский

Универсально полная Yoneda-прешефа сохраняет конечные произведения.

LaTeX

$$$\\text{yonedaPresheaf}'(Y) \\text{ preserves finite products}.$$$

Lean4

/-- The universe polymorphic Yoneda presheaf on `TopCat` preserves finite products. -/
noncomputable instance : PreservesFiniteProducts (yonedaPresheaf'.{w, w'} Y) where
  preserves
    _ :=
    {
      preservesLimit := fun {K} =>
        have :
          ∀ {α : Type} (X : α → TopCat),
            PreservesLimit (Discrete.functor (fun x ↦ op (X x))) (yonedaPresheaf'.{w, w'} Y) :=
          fun X =>
          @PreservesProduct.of_iso_comparison _ _ _ _ (yonedaPresheaf' Y) _ (fun x ↦ op (X x)) _ _
            (by rw [piComparison_fac]; infer_instance)
        let i : K ≅ Discrete.functor (fun i ↦ op (unop (K.obj ⟨i⟩))) := Discrete.natIsoFunctor
        preservesLimit_of_iso_diagram _ i.symm }

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