Documentation

Mathlib.CategoryTheory.Functor.Flat

Representably flat functors #

We define representably flat functors as functors such that the category of structured arrows over X is cofiltered for each X. This concept is also known as flat functors as in [Joh02] Remark C2.3.7, and this name is suggested by Mike Shulman in https://golem.ph.utexas.edu/category/2011/06/flat_functors_and_morphisms_of.html to avoid confusion with other notions of flatness.

This definition is equivalent to left exact functors (functors that preserves finite limits) when C has all finite limits.

Main results #

A functor F : C ⥤ D is representably-flat functor if the comma category (X/F) is cofiltered for each X : C.

Instances

    (Implementation). Given a limit cone c : cone K and a cone s : cone (K ⋙ F) with F representably flat, s can factor through F.mapCone c.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem CategoryTheory.PreservesFiniteLimitsOfFlat.uniq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type v₁} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F] {K : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone K} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone (K.comp F)) (f₁ : s.pt F.obj c.pt) (f₂ : s.pt F.obj c.pt) (h₁ : ∀ (j : J), CategoryTheory.CategoryStruct.comp f₁ ((F.mapCone c).app j) = s.app j) (h₂ : ∀ (j : J), CategoryTheory.CategoryStruct.comp f₂ ((F.mapCone c).app j) = s.app j) :
      f₁ = f₂

      Representably flat functors preserve finite limits.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        If C is finitely cocomplete, then F : C ⥤ D is representably flat iff it preserves finite limits.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          (Implementation) The evaluation of F.lan at X is the colimit over the costructured arrows over X.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            If F : C ⥤ D is a representably flat functor between small categories, then the functor Lan F.op that takes presheaves over C to presheaves over D preserves finite limits.

            Equations
            • One or more equations did not get rendered due to their size.

            If C is finitely complete, then F : C ⥤ D preserves finite limits iff Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*) preserves finite limits.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For