Type-valued flat functors

A functor F : C ⥤ Type w is a flat Type-valued functor if the category F.Elements is cofiltered. (This is not equivalent to saying that F is representably flat in the sense of the typeclass RepresentablyFlat defined in the file Mathlib/CategoryTheory/Functor/Flat.lean, see also https://golem.ph.utexas.edu/category/2011/06/flat_functors_and_morphisms_of.html for a clarification about the differences between these notions.)

In this file, we show that if finite limits exist in C and are preserved by F, then F.Elements is cofiltered.

theorem CategoryTheory.Functor.isCofiltered_elements {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) [Limits.HasFiniteLimits C] [Limits.PreservesFiniteLimits F] : IsCofiltered F.Elements

def CategoryTheory.FunctorToTypes.fromOverSubfunctor {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X : C} (x : F.obj X) : Subfunctor ((Over.forget X).comp F)

Given a functor F : C ⥤ Type w, an object X : C and x : F.obj X, this is the subfunctor of the functor Over.forget X ⋙ F : Over X ⥤ Type w which sends an object of Over X corresponding to a morphism f : Y ⟶ X to the subset of F.obj Y consisting of those elements y : F.obj Y such that F.map f y = x.

Equations

• CategoryTheory.FunctorToTypes.fromOverSubfunctor F x = { obj := fun (U : CategoryTheory.Over X) => F.map U.hom ⁻¹' {x}, map := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.mem_fromOverSubfunctor_iff {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X : C} (x : F.obj X) {U : Over X} (u : F.obj U.left) : u ∈ (fromOverSubfunctor F x).obj U ↔ F.map U.hom u = x

@[reducible, inline]

abbrev CategoryTheory.FunctorToTypes.fromOverFunctor {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X : C} (x : F.obj X) : Functor (Over X) (Type w)

Given a functor F : C ⥤ Type w, an object X : C and x : F.obj X, this is the functor Over X ⥤ Type w which sends an object of Over X corresponding to a morphism f : Y ⟶ X to the subtype of F.obj Y consisting of those elements y : F.obj Y such that F.map f y = x.

Equations

• CategoryTheory.FunctorToTypes.fromOverFunctor F x = (CategoryTheory.FunctorToTypes.fromOverSubfunctor F x).toFunctor

def CategoryTheory.FunctorToTypes.fromOverFunctorElementsEquivalence {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X : C} (x : F.obj X) : (fromOverFunctor F x).Elements ≌ Over (F.elementsMk X x)

Given a functor F : C ⥤ Type w, an object X : C and x : F.obj X, this is the equivalence between the category of elements of fromOverFunctor F x with the Over category of x considered as an object of F.Elements.

Equations

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

instance CategoryTheory.FunctorToTypes.instIsCofilteredElementsOverFromOverFunctor {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X : C} (x : F.obj X) [IsCofiltered F.Elements] : IsCofiltered (fromOverFunctor F x).Elements