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.

Equations

• CategoryTheory.Limits.WalkingCospan = CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingCospan.left : CategoryTheory.Limits.WalkingCospan

The left point of the walking cospan.

Equations

• CategoryTheory.Limits.WalkingCospan.left = some CategoryTheory.Limits.WalkingPair.left

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingCospan.right : CategoryTheory.Limits.WalkingCospan

The right point of the walking cospan.

Equations

• CategoryTheory.Limits.WalkingCospan.right = some CategoryTheory.Limits.WalkingPair.right

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingCospan.one : CategoryTheory.Limits.WalkingCospan

The central point of the walking cospan.

Equations

• CategoryTheory.Limits.WalkingCospan.one = none

@[reducible, inline]

abbrev CategoryTheory.Limits.WalkingSpan : Type

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

Equations

• CategoryTheory.Limits.WalkingSpan = CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingSpan.left : CategoryTheory.Limits.WalkingSpan

The left point of the walking span.

Equations

• CategoryTheory.Limits.WalkingSpan.left = some CategoryTheory.Limits.WalkingPair.left

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingSpan.right : CategoryTheory.Limits.WalkingSpan

The right point of the walking span.

Equations

• CategoryTheory.Limits.WalkingSpan.right = some CategoryTheory.Limits.WalkingPair.right

@[reducible, match_pattern, inline]

abbrev CategoryTheory.Limits.WalkingSpan.zero : CategoryTheory.Limits.WalkingSpan

The central point of the walking span.

Equations

• CategoryTheory.Limits.WalkingSpan.zero = none

@[reducible, inline]

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

The type of arrows for the diagram indexing a pullback.

Equations

• CategoryTheory.Limits.WalkingCospan.Hom = CategoryTheory.Limits.WidePullbackShape.Hom

@[reducible, match_pattern, inline]

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

The left arrow of the walking cospan.

Equations

• CategoryTheory.Limits.WalkingCospan.Hom.inl = CategoryTheory.Limits.WidePullbackShape.Hom.term CategoryTheory.Limits.WalkingPair.left

@[reducible, match_pattern, inline]

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

The right arrow of the walking cospan.

Equations

• CategoryTheory.Limits.WalkingCospan.Hom.inr = CategoryTheory.Limits.WidePullbackShape.Hom.term CategoryTheory.Limits.WalkingPair.right

@[reducible, match_pattern, inline]

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

The identity arrows of the walking cospan.

Equations

• CategoryTheory.Limits.WalkingCospan.Hom.id X = CategoryTheory.Limits.WidePullbackShape.Hom.id X

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

Equations

• ⋯ = ⋯

@[reducible, inline]

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

The type of arrows for the diagram indexing a pushout.

Equations

• CategoryTheory.Limits.WalkingSpan.Hom = CategoryTheory.Limits.WidePushoutShape.Hom

@[reducible, match_pattern, inline]

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

The left arrow of the walking span.

Equations

• CategoryTheory.Limits.WalkingSpan.Hom.fst = CategoryTheory.Limits.WidePushoutShape.Hom.init CategoryTheory.Limits.WalkingPair.left

@[reducible, match_pattern, inline]

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

The right arrow of the walking span.

Equations

• CategoryTheory.Limits.WalkingSpan.Hom.snd = CategoryTheory.Limits.WidePushoutShape.Hom.init CategoryTheory.Limits.WalkingPair.right

@[reducible, match_pattern, inline]

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

The identity arrows of the walking span.

Equations

• CategoryTheory.Limits.WalkingSpan.Hom.id X = CategoryTheory.Limits.WidePushoutShape.Hom.id X

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.Limits.WalkingCospan.ext i w₁ w₂ = CategoryTheory.Limits.Cones.ext i ⋯

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

Equations

• CategoryTheory.Limits.WalkingSpan.ext i w₁ w₂ = CategoryTheory.Limits.Cocones.ext i ⋯

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

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.diagramIsoCospan F = CategoryTheory.NatIso.ofComponents (fun (j : CategoryTheory.Limits.WalkingCospan) => CategoryTheory.eqToIso ⋯) ⋯

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.diagramIsoSpan F = CategoryTheory.NatIso.ofComponents (fun (j : CategoryTheory.Limits.WalkingSpan) => CategoryTheory.eqToIso ⋯) ⋯

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

A functor applied to a cospan is a cospan.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

A functor applied to a span is a span.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Construct an isomorphism of cospans from components.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Construct an isomorphism of spans from components.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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