Guitart exact squares involving Over categories

Let F : C ⥤ D be a functor and X : C. One may consider the commutative square of categories where vertical functors are Over.forget:

    Over.post F
Over X ⥤ Over (F.obj X)
 |          |
 v          v
 C     ⥤    D
       F

We show that this square is Guitart exact if for all Y : C, the binary product X ⨯ Y exists and F commutes with it.

@[reducible, inline]

abbrev CategoryTheory.TwoSquare.overPost {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) : TwoSquare (Over.post F) (Over.forget X) (Over.forget (F.obj X)) F

Given F : C ⥤ D and X : C, this is the 2-square

    Over.post F
Over X ⥤ Over (F.obj X)
 |          |
 v          v
 C     ⥤    D
       F

with Over.forget as vertical functors.

Equations

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

instance CategoryTheory.instGuitartExactOverObjOverPostOfHasBinaryProductOfPreservesLimitDiscreteWalkingPairPair {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) [∀ (Y : C), Limits.HasBinaryProduct X Y] [∀ (Y : C), Limits.PreservesLimit (Limits.pair X Y) F] : (TwoSquare.overPost F X).GuitartExact