Structures · Category theory

CategoryTheory.TwoSquare.GuitartExact

Condition on w : TwoSquare T L R B expressing that it is a Guitart exact square. It is equivalent to saying that for any X₃ : C₃, the induced functor CostructuredArrow L X₃ ⥤ CostructuredArrow R (B.obj X₃) is final (see guitartExact_iff_final) or equivalently that for any X₂ : C₂, the induced functor StructuredArrow X₂ T ⥤ StructuredArrow (R.obj X₂) B is initial (see guitartExact_iff_initial). See also guitartExact_iff_isConnected_rightwards, guitartExact_iff_isConnected_downwards for characterizations in terms of the connectedness of auxiliary categories.

Defined in

Mathlib.CategoryTheory.GuitartExact.Basic

Shape

One type argument · adds isConnected_rightwards