Cospan & Span

We define a category WalkingCospan (resp. WalkingSpan), which is the index category for the given data for a pullback (resp. pushout) diagram. Convenience methods cospan f g and span f g construct functors from the walking (co)span, hitting the given morphisms.

References

• Stacks: Fibre products
• Stacks: Pushouts

@[reducible, inline]

abbrev CategoryTheory.Limits.WalkingCospan : Type

The type of objects for the diagram indexing a pullback, defined as a special case of WidePullbackShape.

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingCospan.left : WalkingCospan

The left point of the walking cospan.

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingCospan.right : WalkingCospan

The right point of the walking cospan.

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingCospan.one : WalkingCospan

The central point of the walking cospan.

@[reducible, inline]

abbrev CategoryTheory.Limits.WalkingSpan : Type

The type of objects for the diagram indexing a pushout, defined as a special case of WidePushoutShape.

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingSpan.left : WalkingSpan

The left point of the walking span.

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingSpan.right : WalkingSpan

The right point of the walking span.

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingSpan.zero : WalkingSpan

The central point of the walking span.

@[reducible, inline]

abbrev CategoryTheory.Limits.WalkingCospan.Hom : WalkingCospan → WalkingCospan → Type

The type of arrows for the diagram indexing a pullback.

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingCospan.Hom.inl : left ⟶ one

The left arrow of the walking cospan.

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingCospan.Hom.inr : right ⟶ one

The right arrow of the walking cospan.

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingCospan.Hom.id (X : WalkingCospan) : X ⟶ X

The identity arrows of the walking cospan.

instance CategoryTheory.Limits.WalkingCospan.instSubsingletonHom (X Y : WalkingCospan) : Subsingleton (X ⟶ Y)

@[reducible, inline]

abbrev CategoryTheory.Limits.WalkingSpan.Hom : WalkingSpan → WalkingSpan → Type

The type of arrows for the diagram indexing a pushout.

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingSpan.Hom.fst : zero ⟶ left

The left arrow of the walking span.

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingSpan.Hom.snd : zero ⟶ right

The right arrow of the walking span.

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingSpan.Hom.id (X : WalkingSpan) : X ⟶ X

The identity arrows of the walking span.

instance CategoryTheory.Limits.WalkingSpan.instSubsingletonHom (X Y : WalkingSpan) : Subsingleton (X ⟶ Y)

def CategoryTheory.Limits.WalkingCospan.ext {C : Type u} [Category.{v, u} C] {F : Functor WalkingCospan C} {s t : Cone F} (i : s.pt ≅ t.pt) (w₁ : s.π.app left = CategoryStruct.comp i.hom (t.π.app left)) (w₂ : s.π.app right = CategoryStruct.comp i.hom (t.π.app right)) : s ≅ t

To construct an isomorphism of cones over the walking cospan, it suffices to construct an isomorphism of the cone points and check it commutes with the legs to left and right.

def CategoryTheory.Limits.WalkingSpan.ext {C : Type u} [Category.{v, u} C] {F : Functor WalkingSpan C} {s t : Cocone F} (i : s.pt ≅ t.pt) (w₁ : CategoryStruct.comp (s.ι.app WalkingCospan.left) i.hom = t.ι.app WalkingCospan.left) (w₂ : CategoryStruct.comp (s.ι.app WalkingCospan.right) i.hom = t.ι.app WalkingCospan.right) : s ≅ t

To construct an isomorphism of cocones over the walking span, it suffices to construct an isomorphism of the cocone points and check it commutes with the legs from left and right.

def CategoryTheory.Limits.cospan {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : Functor WalkingCospan C

cospan f g is the functor from the walking cospan hitting f and g.

def CategoryTheory.Limits.span {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : Functor WalkingSpan C

span f g is the functor from the walking span hitting f and g.

@[simp]

theorem CategoryTheory.Limits.cospan_left {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).obj WalkingCospan.left = X

@[simp]

theorem CategoryTheory.Limits.span_left {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).obj WalkingSpan.left = Y

@[simp]

theorem CategoryTheory.Limits.cospan_right {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).obj WalkingCospan.right = Y

@[simp]

theorem CategoryTheory.Limits.span_right {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).obj WalkingSpan.right = Z

@[simp]

theorem CategoryTheory.Limits.cospan_one {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).obj WalkingCospan.one = Z

@[simp]

theorem CategoryTheory.Limits.span_zero {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).obj WalkingSpan.zero = X

@[simp]

theorem CategoryTheory.Limits.cospan_map_inl {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).map WalkingCospan.Hom.inl = f

@[simp]

theorem CategoryTheory.Limits.span_map_fst {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).map WalkingSpan.Hom.fst = f

@[simp]

theorem CategoryTheory.Limits.cospan_map_inr {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).map WalkingCospan.Hom.inr = g

@[simp]

theorem CategoryTheory.Limits.span_map_snd {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).map WalkingSpan.Hom.snd = g

theorem CategoryTheory.Limits.cospan_map_id {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (w : WalkingCospan) : (cospan f g).map (WalkingCospan.Hom.id w) = CategoryStruct.id ((cospan f g).obj w)

theorem CategoryTheory.Limits.span_map_id {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (w : WalkingSpan) : (span f g).map (WalkingSpan.Hom.id w) = CategoryStruct.id ((span f g).obj w)

def CategoryTheory.Limits.diagramIsoCospan {C : Type u} [Category.{v, u} C] (F : Functor WalkingCospan C) : F ≅ cospan (F.map WalkingCospan.Hom.inl) (F.map WalkingCospan.Hom.inr)

Every diagram indexing a pullback is naturally isomorphic (actually, equal) to a cospan

@[simp]

theorem CategoryTheory.Limits.diagramIsoCospan_inv_app {C : Type u} [Category.{v, u} C] (F : Functor WalkingCospan C) (X : WalkingCospan) : (diagramIsoCospan F).inv.app X = ((fun (j : WalkingCospan) => eqToIso ⋯) X).inv

@[simp]

theorem CategoryTheory.Limits.diagramIsoCospan_hom_app {C : Type u} [Category.{v, u} C] (F : Functor WalkingCospan C) (X : WalkingCospan) : (diagramIsoCospan F).hom.app X = ((fun (j : WalkingCospan) => eqToIso ⋯) X).hom

def CategoryTheory.Limits.diagramIsoSpan {C : Type u} [Category.{v, u} C] (F : Functor WalkingSpan C) : F ≅ span (F.map WalkingSpan.Hom.fst) (F.map WalkingSpan.Hom.snd)

Every diagram indexing a pushout is naturally isomorphic (actually, equal) to a span

@[simp]

theorem CategoryTheory.Limits.diagramIsoSpan_inv_app {C : Type u} [Category.{v, u} C] (F : Functor WalkingSpan C) (X : WalkingSpan) : (diagramIsoSpan F).inv.app X = ((fun (j : WalkingSpan) => eqToIso ⋯) X).inv

@[simp]

theorem CategoryTheory.Limits.diagramIsoSpan_hom_app {C : Type u} [Category.{v, u} C] (F : Functor WalkingSpan C) (X : WalkingSpan) : (diagramIsoSpan F).hom.app X = ((fun (j : WalkingSpan) => eqToIso ⋯) X).hom

def CategoryTheory.Limits.cospanCompIso {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).comp F ≅ cospan (F.map f) (F.map g)

A functor applied to a cospan is a cospan.

@[simp]

theorem CategoryTheory.Limits.cospanCompIso_app_left {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospanCompIso F f g).app WalkingCospan.left = Iso.refl (((cospan f g).comp F).obj WalkingCospan.left)

@[simp]

theorem CategoryTheory.Limits.cospanCompIso_app_right {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospanCompIso F f g).app WalkingCospan.right = Iso.refl (((cospan f g).comp F).obj WalkingCospan.right)

@[simp]

theorem CategoryTheory.Limits.cospanCompIso_app_one {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospanCompIso F f g).app WalkingCospan.one = Iso.refl (((cospan f g).comp F).obj WalkingCospan.one)

@[simp]

theorem CategoryTheory.Limits.cospanCompIso_hom_app_left {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospanCompIso F f g).hom.app WalkingCospan.left = CategoryStruct.id (((cospan f g).comp F).obj WalkingCospan.left)

@[simp]

theorem CategoryTheory.Limits.cospanCompIso_hom_app_right {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospanCompIso F f g).hom.app WalkingCospan.right = CategoryStruct.id (((cospan f g).comp F).obj WalkingCospan.right)

@[simp]

theorem CategoryTheory.Limits.cospanCompIso_hom_app_one {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospanCompIso F f g).hom.app WalkingCospan.one = CategoryStruct.id (((cospan f g).comp F).obj WalkingCospan.one)

@[simp]

theorem CategoryTheory.Limits.cospanCompIso_inv_app_left {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospanCompIso F f g).inv.app WalkingCospan.left = CategoryStruct.id ((cospan (F.map f) (F.map g)).obj WalkingCospan.left)

@[simp]

theorem CategoryTheory.Limits.cospanCompIso_inv_app_right {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospanCompIso F f g).inv.app WalkingCospan.right = CategoryStruct.id ((cospan (F.map f) (F.map g)).obj WalkingCospan.right)

@[simp]

theorem CategoryTheory.Limits.cospanCompIso_inv_app_one {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospanCompIso F f g).inv.app WalkingCospan.one = CategoryStruct.id ((cospan (F.map f) (F.map g)).obj WalkingCospan.one)

def CategoryTheory.Limits.spanCompIso {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).comp F ≅ span (F.map f) (F.map g)

A functor applied to a span is a span.

@[simp]

theorem CategoryTheory.Limits.spanCompIso_app_left {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (spanCompIso F f g).app WalkingSpan.left = Iso.refl (((span f g).comp F).obj WalkingSpan.left)

@[simp]

theorem CategoryTheory.Limits.spanCompIso_app_right {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (spanCompIso F f g).app WalkingSpan.right = Iso.refl (((span f g).comp F).obj WalkingSpan.right)

@[simp]

theorem CategoryTheory.Limits.spanCompIso_app_zero {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (spanCompIso F f g).app WalkingSpan.zero = Iso.refl (((span f g).comp F).obj WalkingSpan.zero)

@[simp]

theorem CategoryTheory.Limits.spanCompIso_hom_app_left {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (spanCompIso F f g).hom.app WalkingSpan.left = CategoryStruct.id (((span f g).comp F).obj WalkingSpan.left)

@[simp]

theorem CategoryTheory.Limits.spanCompIso_hom_app_right {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (spanCompIso F f g).hom.app WalkingSpan.right = CategoryStruct.id (((span f g).comp F).obj WalkingSpan.right)

@[simp]

theorem CategoryTheory.Limits.spanCompIso_hom_app_zero {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (spanCompIso F f g).hom.app WalkingSpan.zero = CategoryStruct.id (((span f g).comp F).obj WalkingSpan.zero)

@[simp]

theorem CategoryTheory.Limits.spanCompIso_inv_app_left {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (spanCompIso F f g).inv.app WalkingSpan.left = CategoryStruct.id ((span (F.map f) (F.map g)).obj WalkingSpan.left)

@[simp]

theorem CategoryTheory.Limits.spanCompIso_inv_app_right {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (spanCompIso F f g).inv.app WalkingSpan.right = CategoryStruct.id ((span (F.map f) (F.map g)).obj WalkingSpan.right)

@[simp]

theorem CategoryTheory.Limits.spanCompIso_inv_app_zero {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (spanCompIso F f g).inv.app WalkingSpan.zero = CategoryStruct.id ((span (F.map f) (F.map g)).obj WalkingSpan.zero)

def CategoryTheory.Limits.cospanHomMk {C : Type u} [Category.{v, u} C] {F G : Functor WalkingCospan C} (z : F.obj WalkingCospan.one ⟶ G.obj WalkingCospan.one) (l : F.obj WalkingCospan.left ⟶ G.obj WalkingCospan.left) (r : F.obj WalkingCospan.right ⟶ G.obj WalkingCospan.right) (hl : CategoryStruct.comp (F.map WalkingCospan.Hom.inl) z = CategoryStruct.comp l (G.map WalkingCospan.Hom.inl) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingCospan.Hom.inr) z = CategoryStruct.comp r (G.map WalkingCospan.Hom.inr) := by cat_disch) : F ⟶ G

Constructor for natural transformations between cospans.

@[simp]

theorem CategoryTheory.Limits.cospanHomMk_app {C : Type u} [Category.{v, u} C] {F G : Functor WalkingCospan C} (z : F.obj WalkingCospan.one ⟶ G.obj WalkingCospan.one) (l : F.obj WalkingCospan.left ⟶ G.obj WalkingCospan.left) (r : F.obj WalkingCospan.right ⟶ G.obj WalkingCospan.right) (hl : CategoryStruct.comp (F.map WalkingCospan.Hom.inl) z = CategoryStruct.comp l (G.map WalkingCospan.Hom.inl) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingCospan.Hom.inr) z = CategoryStruct.comp r (G.map WalkingCospan.Hom.inr) := by cat_disch) (X✝ : WalkingCospan) : (cospanHomMk z l r hl hr).app X✝ = Option.casesOn X✝ z fun (val : WalkingPair) => WalkingPair.casesOn val l r

def CategoryTheory.Limits.cospanIsoMk {C : Type u} [Category.{v, u} C] {F G : Functor WalkingCospan C} (z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one) (l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left) (r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right) (hl : CategoryStruct.comp (F.map WalkingCospan.Hom.inl) z.hom = CategoryStruct.comp l.hom (G.map WalkingCospan.Hom.inl) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingCospan.Hom.inr) z.hom = CategoryStruct.comp r.hom (G.map WalkingCospan.Hom.inr) := by cat_disch) : F ≅ G

Constructor for natural isomorphisms between cospans.

@[simp]

theorem CategoryTheory.Limits.cospanIsoMk_hom_app {C : Type u} [Category.{v, u} C] {F G : Functor WalkingCospan C} (z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one) (l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left) (r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right) (hl : CategoryStruct.comp (F.map WalkingCospan.Hom.inl) z.hom = CategoryStruct.comp l.hom (G.map WalkingCospan.Hom.inl) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingCospan.Hom.inr) z.hom = CategoryStruct.comp r.hom (G.map WalkingCospan.Hom.inr) := by cat_disch) (X : WalkingCospan) : (cospanIsoMk z l r hl hr).hom.app X = (Option.rec z (fun (val : WalkingPair) => WalkingPair.rec l r val) X).hom

@[simp]

theorem CategoryTheory.Limits.cospanIsoMk_inv_app {C : Type u} [Category.{v, u} C] {F G : Functor WalkingCospan C} (z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one) (l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left) (r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right) (hl : CategoryStruct.comp (F.map WalkingCospan.Hom.inl) z.hom = CategoryStruct.comp l.hom (G.map WalkingCospan.Hom.inl) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingCospan.Hom.inr) z.hom = CategoryStruct.comp r.hom (G.map WalkingCospan.Hom.inr) := by cat_disch) (X : WalkingCospan) : (cospanIsoMk z l r hl hr).inv.app X = (Option.rec z (fun (val : WalkingPair) => WalkingPair.rec l r val) X).inv

def CategoryTheory.Limits.cospanExt {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iZ.hom) (wg : CategoryStruct.comp iY.hom g' = CategoryStruct.comp g iZ.hom) : cospan f g ≅ cospan f' g'

Construct an isomorphism of cospans from components.

@[simp]

theorem CategoryTheory.Limits.cospanExt_app_left {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iZ.hom) (wg : CategoryStruct.comp iY.hom g' = CategoryStruct.comp g iZ.hom) : (cospanExt iX iY iZ wf wg).app WalkingCospan.left = iX

@[simp]

theorem CategoryTheory.Limits.cospanExt_app_right {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iZ.hom) (wg : CategoryStruct.comp iY.hom g' = CategoryStruct.comp g iZ.hom) : (cospanExt iX iY iZ wf wg).app WalkingCospan.right = iY

@[simp]

theorem CategoryTheory.Limits.cospanExt_app_one {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iZ.hom) (wg : CategoryStruct.comp iY.hom g' = CategoryStruct.comp g iZ.hom) : (cospanExt iX iY iZ wf wg).app WalkingCospan.one = iZ

@[simp]

theorem CategoryTheory.Limits.cospanExt_hom_app_left {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iZ.hom) (wg : CategoryStruct.comp iY.hom g' = CategoryStruct.comp g iZ.hom) : (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.left = iX.hom

@[simp]

theorem CategoryTheory.Limits.cospanExt_hom_app_right {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iZ.hom) (wg : CategoryStruct.comp iY.hom g' = CategoryStruct.comp g iZ.hom) : (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.right = iY.hom

@[simp]

theorem CategoryTheory.Limits.cospanExt_hom_app_one {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iZ.hom) (wg : CategoryStruct.comp iY.hom g' = CategoryStruct.comp g iZ.hom) : (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.one = iZ.hom

@[simp]

theorem CategoryTheory.Limits.cospanExt_inv_app_left {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iZ.hom) (wg : CategoryStruct.comp iY.hom g' = CategoryStruct.comp g iZ.hom) : (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.left = iX.inv

@[simp]

theorem CategoryTheory.Limits.cospanExt_inv_app_right {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iZ.hom) (wg : CategoryStruct.comp iY.hom g' = CategoryStruct.comp g iZ.hom) : (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.right = iY.inv

@[simp]

theorem CategoryTheory.Limits.cospanExt_inv_app_one {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iZ.hom) (wg : CategoryStruct.comp iY.hom g' = CategoryStruct.comp g iZ.hom) : (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.one = iZ.inv

def CategoryTheory.Limits.spanHomMk {C : Type u} [Category.{v, u} C] {F G : Functor WalkingSpan C} (z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero) (l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left) (r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right) (hl : CategoryStruct.comp (F.map WalkingSpan.Hom.fst) l = CategoryStruct.comp z (G.map WalkingSpan.Hom.fst) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingSpan.Hom.snd) r = CategoryStruct.comp z (G.map WalkingSpan.Hom.snd) := by cat_disch) : F ⟶ G

Constructor for natural transformations between spans.

@[simp]

theorem CategoryTheory.Limits.spanHomMk_app {C : Type u} [Category.{v, u} C] {F G : Functor WalkingSpan C} (z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero) (l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left) (r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right) (hl : CategoryStruct.comp (F.map WalkingSpan.Hom.fst) l = CategoryStruct.comp z (G.map WalkingSpan.Hom.fst) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingSpan.Hom.snd) r = CategoryStruct.comp z (G.map WalkingSpan.Hom.snd) := by cat_disch) (X✝ : WalkingSpan) : (spanHomMk z l r hl hr).app X✝ = Option.casesOn X✝ z fun (val : WalkingPair) => WalkingPair.casesOn val l r

def CategoryTheory.Limits.spanIsoMk {C : Type u} [Category.{v, u} C] {F G : Functor WalkingSpan C} (z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero) (l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left) (r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right) (hl : CategoryStruct.comp (F.map WalkingSpan.Hom.fst) l.hom = CategoryStruct.comp z.hom (G.map WalkingSpan.Hom.fst) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingSpan.Hom.snd) r.hom = CategoryStruct.comp z.hom (G.map WalkingSpan.Hom.snd) := by cat_disch) : F ≅ G

Constructor for natural isomorphisms between spans.

@[simp]

theorem CategoryTheory.Limits.spanIsoMk_hom_app {C : Type u} [Category.{v, u} C] {F G : Functor WalkingSpan C} (z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero) (l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left) (r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right) (hl : CategoryStruct.comp (F.map WalkingSpan.Hom.fst) l.hom = CategoryStruct.comp z.hom (G.map WalkingSpan.Hom.fst) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingSpan.Hom.snd) r.hom = CategoryStruct.comp z.hom (G.map WalkingSpan.Hom.snd) := by cat_disch) (X : WalkingSpan) : (spanIsoMk z l r hl hr).hom.app X = (Option.rec z (fun (val : WalkingPair) => WalkingPair.rec l r val) X).hom

@[simp]

theorem CategoryTheory.Limits.spanIsoMk_inv_app {C : Type u} [Category.{v, u} C] {F G : Functor WalkingSpan C} (z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero) (l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left) (r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right) (hl : CategoryStruct.comp (F.map WalkingSpan.Hom.fst) l.hom = CategoryStruct.comp z.hom (G.map WalkingSpan.Hom.fst) := by cat_disch) (hr : CategoryStruct.comp (F.map WalkingSpan.Hom.snd) r.hom = CategoryStruct.comp z.hom (G.map WalkingSpan.Hom.snd) := by cat_disch) (X : WalkingSpan) : (spanIsoMk z l r hl hr).inv.app X = (Option.rec z (fun (val : WalkingPair) => WalkingPair.rec l r val) X).inv

def CategoryTheory.Limits.spanExt {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iY.hom) (wg : CategoryStruct.comp iX.hom g' = CategoryStruct.comp g iZ.hom) : span f g ≅ span f' g'

Construct an isomorphism of spans from components.

@[simp]

theorem CategoryTheory.Limits.spanExt_app_left {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iY.hom) (wg : CategoryStruct.comp iX.hom g' = CategoryStruct.comp g iZ.hom) : (spanExt iX iY iZ wf wg).app WalkingSpan.left = iY

@[simp]

theorem CategoryTheory.Limits.spanExt_app_right {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iY.hom) (wg : CategoryStruct.comp iX.hom g' = CategoryStruct.comp g iZ.hom) : (spanExt iX iY iZ wf wg).app WalkingSpan.right = iZ

@[simp]

theorem CategoryTheory.Limits.spanExt_app_one {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iY.hom) (wg : CategoryStruct.comp iX.hom g' = CategoryStruct.comp g iZ.hom) : (spanExt iX iY iZ wf wg).app WalkingSpan.zero = iX

@[simp]

theorem CategoryTheory.Limits.spanExt_hom_app_left {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iY.hom) (wg : CategoryStruct.comp iX.hom g' = CategoryStruct.comp g iZ.hom) : (spanExt iX iY iZ wf wg).hom.app WalkingSpan.left = iY.hom

@[simp]

theorem CategoryTheory.Limits.spanExt_hom_app_right {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iY.hom) (wg : CategoryStruct.comp iX.hom g' = CategoryStruct.comp g iZ.hom) : (spanExt iX iY iZ wf wg).hom.app WalkingSpan.right = iZ.hom

@[simp]

theorem CategoryTheory.Limits.spanExt_hom_app_zero {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iY.hom) (wg : CategoryStruct.comp iX.hom g' = CategoryStruct.comp g iZ.hom) : (spanExt iX iY iZ wf wg).hom.app WalkingSpan.zero = iX.hom

@[simp]

theorem CategoryTheory.Limits.spanExt_inv_app_left {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iY.hom) (wg : CategoryStruct.comp iX.hom g' = CategoryStruct.comp g iZ.hom) : (spanExt iX iY iZ wf wg).inv.app WalkingSpan.left = iY.inv

@[simp]

theorem CategoryTheory.Limits.spanExt_inv_app_right {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iY.hom) (wg : CategoryStruct.comp iX.hom g' = CategoryStruct.comp g iZ.hom) : (spanExt iX iY iZ wf wg).inv.app WalkingSpan.right = iZ.inv

@[simp]

theorem CategoryTheory.Limits.spanExt_inv_app_zero {C : Type u} [Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} (wf : CategoryStruct.comp iX.hom f' = CategoryStruct.comp f iY.hom) (wg : CategoryStruct.comp iX.hom g' = CategoryStruct.comp g iZ.hom) : (spanExt iX iY iZ wf wg).inv.app WalkingSpan.zero = iX.inv