Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

CategoryTheory.Limits.WalkingCospan abbrev

: Type

Full source

/-- The type of objects for the diagram indexing a pullback, defined as a special case of
`WidePullbackShape`. -/
abbrev WalkingCospan : Type :=
  WidePullbackShape WalkingPair

Indexing Category for Pullback Diagrams

Informal description

The type `WalkingCospan` represents the indexing category for a pullback diagram, consisting of three objects: the left object, the right object, and their common target object.

CategoryTheory.Limits.WalkingCospan.left abbrev

: WalkingCospan

Full source

/-- The left point of the walking cospan. -/
@[match_pattern]
abbrev WalkingCospan.left : WalkingCospan :=
  some WalkingPair.left

Left object of walking cospan category

Informal description

The left object in the indexing category `WalkingCospan` used for pullback diagrams.

CategoryTheory.Limits.WalkingCospan.right abbrev

: WalkingCospan

Full source

/-- The right point of the walking cospan. -/
@[match_pattern]
abbrev WalkingCospan.right : WalkingCospan :=
  some WalkingPair.right

Right object of walking cospan

Informal description

The right object in the walking cospan indexing category for pullback diagrams.

CategoryTheory.Limits.WalkingCospan.one abbrev

: WalkingCospan

Full source

/-- The central point of the walking cospan. -/
@[match_pattern]
abbrev WalkingCospan.one : WalkingCospan :=
  none

Central Object of Walking Cospan

Informal description

The central object in the walking cospan indexing category for pullback diagrams.

CategoryTheory.Limits.WalkingSpan abbrev

: Type

Full source

/-- The type of objects for the diagram indexing a pushout, defined as a special case of
`WidePushoutShape`.
-/
abbrev WalkingSpan : Type :=
  WidePushoutShape WalkingPair

Index Category for Pushout Diagrams (Walking Span)

Informal description

The type `WalkingSpan` is used as the index category for diagrams defining pushout constructions in category theory. It consists of three objects: `left`, `right`, and a central object (often implicit) that serves as the apex of the span.

CategoryTheory.Limits.WalkingSpan.left abbrev

: WalkingSpan

Full source

/-- The left point of the walking span. -/
@[match_pattern]
abbrev WalkingSpan.left : WalkingSpan :=
  some WalkingPair.left

Left Object of Walking Span Category

Informal description

The object `left` in the walking span category, which is one of the three objects (along with `right` and `zero`) used to index pushout diagrams in category theory.

CategoryTheory.Limits.WalkingSpan.right abbrev

: WalkingSpan

Full source

/-- The right point of the walking span. -/
@[match_pattern]
abbrev WalkingSpan.right : WalkingSpan :=
  some WalkingPair.right

Right object in walking span

Informal description

The right object in the walking span index category used for pushout diagrams.

CategoryTheory.Limits.WalkingSpan.zero abbrev

: WalkingSpan

Full source

/-- The central point of the walking span. -/
@[match_pattern]
abbrev WalkingSpan.zero : WalkingSpan :=
  none

Apex of Walking Span Index Category

Informal description

The central object in the walking span index category, denoted as `zero`, which serves as the apex of the span diagram.

CategoryTheory.Limits.WalkingCospan.Hom abbrev

: WalkingCospan → WalkingCospan → Type

Full source

/-- The type of arrows for the diagram indexing a pullback. -/
abbrev Hom : WalkingCospan → WalkingCospan → Type :=
  WidePullbackShape.Hom

Morphisms in the Pullback Indexing Category

Informal description

The type of morphisms in the indexing category `WalkingCospan` for pullback diagrams, which consists of morphisms between objects in `WalkingCospan`. Specifically, it includes the left inclusion morphism `inl : left → one` and the right inclusion morphism `inr : right → one`.

CategoryTheory.Limits.WalkingCospan.Hom.inl abbrev

: left ⟶ one

Full source

/-- The left arrow of the walking cospan. -/
@[match_pattern]
abbrev Hom.inl : leftleft ⟶ one :=
  WidePullbackShape.Hom.term _

Left inclusion morphism in walking cospan category

Informal description

The left inclusion morphism $\mathrm{inl}$ from the left object to the central object in the walking cospan indexing category for pullback diagrams.

CategoryTheory.Limits.WalkingCospan.Hom.inr abbrev

: right ⟶ one

Full source

/-- The right arrow of the walking cospan. -/
@[match_pattern]
abbrev Hom.inr : rightright ⟶ one :=
  WidePullbackShape.Hom.term _

Right Inclusion Morphism in Walking Cospan

Informal description

The right inclusion morphism $\mathrm{inr}$ from the right object to the central object in the walking cospan indexing category for pullback diagrams.

CategoryTheory.Limits.WalkingCospan.Hom.id abbrev

(X : WalkingCospan) : X ⟶ X

Full source

/-- The identity arrows of the walking cospan. -/
@[match_pattern]
abbrev Hom.id (X : WalkingCospan) : X ⟶ X :=
  WidePullbackShape.Hom.id X

Identity morphisms in the walking cospan category

Informal description

For any object $X$ in the walking cospan category, there exists an identity morphism $\mathrm{id}_X : X \to X$.

CategoryTheory.Limits.WalkingCospan.instSubsingletonHom instance

(X Y : WalkingCospan) : Subsingleton (X ⟶ Y)

Full source

instance (X Y : WalkingCospan) : Subsingleton (X ⟶ Y) := by
  constructor; intros; simp [eq_iff_true_of_subsingleton]

Uniqueness of Morphisms in the Walking Cospan Category

Informal description

For any two objects $X$ and $Y$ in the walking cospan category, the set of morphisms from $X$ to $Y$ is a subsingleton (i.e., it has at most one element).

CategoryTheory.Limits.WalkingSpan.Hom abbrev

: WalkingSpan → WalkingSpan → Type

Full source

/-- The type of arrows for the diagram indexing a pushout. -/
abbrev Hom : WalkingSpan → WalkingSpan → Type :=
  WidePushoutShape.Hom

Morphisms in the Walking Span Category

Informal description

The type of morphisms in the category `WalkingSpan`, which serves as the index category for pushout diagrams. For any two objects $X$ and $Y$ in `WalkingSpan`, the type `WalkingSpan.Hom X Y` represents the set of morphisms from $X$ to $Y$.

CategoryTheory.Limits.WalkingSpan.Hom.fst abbrev

: zero ⟶ left

Full source

/-- The left arrow of the walking span. -/
@[match_pattern]
abbrev Hom.fst : zerozero ⟶ left :=
  WidePushoutShape.Hom.init _

First Projection Morphism in Walking Span Category

Informal description

The morphism `fst` in the walking span category represents the first projection from the apex `zero` to the left object `left`.

CategoryTheory.Limits.WalkingSpan.Hom.snd abbrev

: zero ⟶ right

Full source

/-- The right arrow of the walking span. -/
@[match_pattern]
abbrev Hom.snd : zerozero ⟶ right :=
  WidePushoutShape.Hom.init _

Second Projection Morphism in Walking Span Category

Informal description

The morphism $\mathrm{snd}$ in the walking span category represents the second projection from the apex `zero` to the right object `right$.

CategoryTheory.Limits.WalkingSpan.Hom.id abbrev

(X : WalkingSpan) : X ⟶ X

Full source

/-- The identity arrows of the walking span. -/
@[match_pattern]
abbrev Hom.id (X : WalkingSpan) : X ⟶ X :=
  WidePushoutShape.Hom.id X

Identity Morphism in Walking Span Category

Informal description

For any object $X$ in the walking span category, there exists an identity morphism $\mathrm{id}_X : X \to X$.

CategoryTheory.Limits.WalkingSpan.instSubsingletonHom instance

(X Y : WalkingSpan) : Subsingleton (X ⟶ Y)

Full source

instance (X Y : WalkingSpan) : Subsingleton (X ⟶ Y) := by
  constructor; intros a b; simp [eq_iff_true_of_subsingleton]

Uniqueness of Morphisms in Walking Span Category

Informal description

For any two objects $X$ and $Y$ in the walking span category, the hom-set $\mathrm{Hom}(X, Y)$ is a subsingleton (i.e., it has at most one element).

CategoryTheory.Limits.WalkingCospan.ext definition

 {F : WalkingCospan ⥤ C} {s t : Cone F} (i : s.pt ≅ t.pt)
  (w₁ : s.π.app WalkingCospan.left = i.hom ≫ t.π.app WalkingCospan.left)
  (w₂ : s.π.app WalkingCospan.right = i.hom ≫ t.π.app WalkingCospan.right) : s ≅ t

Full source

/-- 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 WalkingCospan.ext {F : WalkingCospanWalkingCospan ⥤ C} {s t : Cone F} (i : s.pt ≅ t.pt)
    (w₁ : s.π.app WalkingCospan.left = i.hom ≫ t.π.app WalkingCospan.left)
    (w₂ : s.π.app WalkingCospan.right = i.hom ≫ t.π.app WalkingCospan.right) : s ≅ t := by
  apply Cones.ext i _
  rintro (⟨⟩ | ⟨⟨⟩⟩)
  · have h₁ := s.π.naturality WalkingCospan.Hom.inl
    dsimp at h₁
    simp only [Category.id_comp] at h₁
    have h₂ := t.π.naturality WalkingCospan.Hom.inl
    dsimp at h₂
    simp only [Category.id_comp] at h₂
    simp_rw [h₂, ← Category.assoc, ← w₁, ← h₁]
  · exact w₁
  · exact w₂

Isomorphism of cones over a cospan

Informal description

Given two cones $s$ and $t$ over a functor $F$ from the walking cospan category to a category $C$, an isomorphism $i$ between their cone points, and proofs that $i$ commutes with the cone legs at the left and right objects, then $s$ and $t$ are isomorphic as cones.

CategoryTheory.Limits.WalkingSpan.ext definition

 {F : WalkingSpan ⥤ C} {s t : Cocone F} (i : s.pt ≅ t.pt)
  (w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left)
  (w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right) : s ≅ t

Full source

/-- 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 WalkingSpan.ext {F : WalkingSpanWalkingSpan ⥤ C} {s t : Cocone F} (i : s.pt ≅ t.pt)
    (w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left)
    (w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right) : s ≅ t := by
  apply Cocones.ext i _
  rintro (⟨⟩ | ⟨⟨⟩⟩)
  · have h₁ := s.ι.naturality WalkingSpan.Hom.fst
    dsimp at h₁
    simp only [Category.comp_id] at h₁
    have h₂ := t.ι.naturality WalkingSpan.Hom.fst
    dsimp at h₂
    simp only [Category.comp_id] at h₂
    simp_rw [← h₁, Category.assoc, w₁, h₂]
  · exact w₁
  · exact w₂

Isomorphism of cocones over a span

Informal description

Given two cocones $s$ and $t$ over a functor $F$ from the walking span category to a category $\mathcal{C}$, and an isomorphism $i : s.\text{pt} \cong t.\text{pt}$ between their cocone points, if the following two conditions hold: 1. The left leg of $s$ composed with $i$ equals the left leg of $t$: $s.\iota.\text{left} \circ i = t.\iota.\text{left}$ 2. The right leg of $s$ composed with $i$ equals the right leg of $t$: $s.\iota.\text{right} \circ i = t.\iota.\text{right}$ then $s$ and $t$ are isomorphic as cocones.

CategoryTheory.Limits.cospan definition

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : WalkingCospan ⥤ C

Full source

/-- `cospan f g` is the functor from the walking cospan hitting `f` and `g`. -/
def cospan {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : WalkingCospanWalkingCospan ⥤ C :=
  WidePullbackShape.wideCospan Z (fun j => WalkingPair.casesOn j X Y) fun j =>
    WalkingPair.casesOn j f g

Cospan functor for pullback diagrams

Informal description

Given objects $X, Y, Z$ in a category $C$ and morphisms $f : X \to Z$, $g : Y \to Z$, the functor `cospan f g` maps the walking cospan indexing category to $C$ by sending the left object to $X$, the right object to $Y$, and the common target object to $Z$, with the morphisms given by $f$ and $g$ respectively.

CategoryTheory.Limits.span definition

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : WalkingSpan ⥤ C

Full source

/-- `span f g` is the functor from the walking span hitting `f` and `g`. -/
def span {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : WalkingSpanWalkingSpan ⥤ C :=
  WidePushoutShape.wideSpan X (fun j => WalkingPair.casesOn j Y Z) fun j =>
    WalkingPair.casesOn j f g

Span functor for pushout diagrams

Informal description

Given objects $X, Y, Z$ in a category $C$ and morphisms $f : X \to Y$, $g : X \to Z$, the functor `span f g` maps the walking span indexing category to $C$ by sending the apex object to $X$, the left object to $Y$, and the right object to $Z$, with the morphisms given by $f$ and $g$ respectively.

CategoryTheory.Limits.cospan_left theorem

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).obj WalkingCospan.left = X

Full source

@[simp]
theorem cospan_left {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).obj WalkingCospan.left = X :=
  rfl

Cospan Functor Maps Left Object to Source of First Morphism

Informal description

For any objects $X, Y, Z$ in a category $C$ and morphisms $f \colon X \to Z$, $g \colon Y \to Z$, the functor $\mathrm{cospan}\, f\, g$ maps the left object of the walking cospan to $X$, i.e., $(\mathrm{cospan}\, f\, g)(\mathrm{left}) = X$.

CategoryTheory.Limits.span_left theorem

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).obj WalkingSpan.left = Y

Full source

@[simp]
theorem span_left {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).obj WalkingSpan.left = Y :=
  rfl

Span Functor Maps Left Object to Target of First Morphism

Informal description

For any objects $X, Y, Z$ in a category $C$ and morphisms $f \colon X \to Y$, $g \colon X \to Z$, the functor $\mathrm{span}\, f\, g$ maps the left object of the walking span to $Y$, i.e., $(\mathrm{span}\, f\, g)(\mathrm{left}) = Y$.

CategoryTheory.Limits.cospan_right theorem

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).obj WalkingCospan.right = Y

Full source

@[simp]
theorem cospan_right {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    (cospan f g).obj WalkingCospan.right = Y := rfl

Cospan Functor Maps Right Object to Source of Second Morphism

Informal description

For any objects $X, Y, Z$ in a category $C$ and morphisms $f : X \to Z$, $g : Y \to Z$, the functor $\mathrm{cospan}\, f\, g$ maps the right object of the walking cospan to $Y$, i.e., $(\mathrm{cospan}\, f\, g)(\mathrm{right}) = Y$.

CategoryTheory.Limits.span_right theorem

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).obj WalkingSpan.right = Z

Full source

@[simp]
theorem span_right {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).obj WalkingSpan.right = Z :=
  rfl

Span functor maps right object to target of second morphism

Informal description

For any objects $X, Y, Z$ in a category $C$ and morphisms $f: X \to Y$, $g: X \to Z$, the functor $\mathrm{span}\, f\, g$ maps the right object of the walking span to $Z$, i.e., $(\mathrm{span}\, f\, g)(\mathrm{right}) = Z$.

CategoryTheory.Limits.cospan_one theorem

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).obj WalkingCospan.one = Z

Full source

@[simp]
theorem cospan_one {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).obj WalkingCospan.one = Z :=
  rfl

Cospan Functor Maps Central Object to Common Target

Informal description

For any objects $X, Y, Z$ in a category $C$ and morphisms $f : X \to Z$, $g : Y \to Z$, the functor $\mathrm{cospan}\, f\, g$ maps the central object of the walking cospan category to $Z$, i.e., $(\mathrm{cospan}\, f\, g)(\mathrm{one}) = Z$.

CategoryTheory.Limits.span_zero theorem

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).obj WalkingSpan.zero = X

Full source

@[simp]
theorem span_zero {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).obj WalkingSpan.zero = X :=
  rfl

Span Functor Maps Apex to Source Object

Informal description

For any objects $X, Y, Z$ in a category $C$ and morphisms $f : X \to Y$, $g : X \to Z$, the functor $\mathrm{span}\, f\, g$ maps the apex object (zero) of the walking span category to $X$, i.e., $(\mathrm{span}\, f\, g)(\mathrm{zero}) = X$.

CategoryTheory.Limits.cospan_map_inl theorem

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).map WalkingCospan.Hom.inl = f

Full source

@[simp]
theorem cospan_map_inl {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    (cospan f g).map WalkingCospan.Hom.inl = f := rfl

Mapping of Left Inclusion in Cospan Functor

Informal description

Given objects $X, Y, Z$ in a category $C$ and morphisms $f : X \to Z$, $g : Y \to Z$, the functor `cospan f g` maps the left inclusion morphism $\mathrm{inl}$ in the walking cospan category to the morphism $f$ in $C$.

CategoryTheory.Limits.span_map_fst theorem

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).map WalkingSpan.Hom.fst = f

Full source

@[simp]
theorem span_map_fst {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).map WalkingSpan.Hom.fst = f :=
  rfl

Functoriality of Span Construction: $\mathrm{span}\, f\, g$ Maps $\mathrm{fst}$ to $f$

Informal description

Given objects $X, Y, Z$ in a category $C$ and morphisms $f : X \to Y$, $g : X \to Z$, the functor $\mathrm{span}\, f\, g$ maps the first projection morphism $\mathrm{fst}$ in the walking span category to the morphism $f$ in $C$.

CategoryTheory.Limits.cospan_map_inr theorem

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).map WalkingCospan.Hom.inr = g

Full source

@[simp]
theorem cospan_map_inr {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    (cospan f g).map WalkingCospan.Hom.inr = g := rfl

Functoriality of Cospan Construction: $\mathrm{cospan}\, f\, g$ Maps $\mathrm{inr}$ to $g$

Informal description

Given objects $X, Y, Z$ in a category $C$ and morphisms $f \colon X \to Z$, $g \colon Y \to Z$, the functor $\mathrm{cospan}\, f\, g$ maps the right inclusion morphism $\mathrm{inr}$ in the walking cospan category to the morphism $g$ in $C$.

CategoryTheory.Limits.span_map_snd theorem

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).map WalkingSpan.Hom.snd = g

Full source

@[simp]
theorem span_map_snd {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).map WalkingSpan.Hom.snd = g :=
  rfl

Functoriality of Span Construction: $\mathrm{span}\, f\, g$ Maps $\mathrm{snd}$ to $g$

Informal description

For any objects $X, Y, Z$ in a category $C$ and morphisms $f : X \to Y$, $g : X \to Z$, the functor $\mathrm{span}\, f\, g$ maps the second projection morphism $\mathrm{snd}$ in the walking span category to the morphism $g$.

CategoryTheory.Limits.cospan_map_id theorem

{X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (w : WalkingCospan) : (cospan f g).map (WalkingCospan.Hom.id w) = 𝟙 _

Full source

theorem cospan_map_id {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (w : WalkingCospan) :
    (cospan f g).map (WalkingCospan.Hom.id w) = 𝟙 _ := rfl

Cospan Functor Preserves Identity Morphisms

Informal description

For any objects $X, Y, Z$ in a category $C$ and morphisms $f : X \to Z$, $g : Y \to Z$, the functor $\mathrm{cospan}\, f\, g$ preserves identity morphisms. That is, for any object $w$ in the walking cospan category, the functor maps the identity morphism $\mathrm{id}_w$ to the identity morphism $\mathrm{id}_{(\mathrm{cospan}\, f\, g)(w)}$ in $C$.

CategoryTheory.Limits.span_map_id theorem

{X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (w : WalkingSpan) : (span f g).map (WalkingSpan.Hom.id w) = 𝟙 _

Full source

theorem span_map_id {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (w : WalkingSpan) :
    (span f g).map (WalkingSpan.Hom.id w) = 𝟙 _ := rfl

Span Functor Preserves Identity Morphisms

Informal description

For any objects $X, Y, Z$ in a category $C$ and morphisms $f : X \to Y$, $g : X \to Z$, the functor $\mathrm{span}\, f\, g$ preserves identity morphisms. That is, for any object $w$ in the walking span category, the functor maps the identity morphism $\mathrm{id}_w$ to the identity morphism $\mathrm{id}_{(\mathrm{span}\, f\, g)(w)}$ in $C$.

CategoryTheory.Limits.diagramIsoCospan definition

(F : WalkingCospan ⥤ C) : F ≅ cospan (F.map inl) (F.map inr)

Full source

/-- Every diagram indexing a pullback is naturally isomorphic (actually, equal) to a `cospan` -/
-- @[simps (config := { rhsMd := semireducible })]  Porting note: no semireducible
@[simps!]
def diagramIsoCospan (F : WalkingCospanWalkingCospan ⥤ C) : F ≅ cospan (F.map inl) (F.map inr) :=
  NatIso.ofComponents
  (fun j => eqToIso (by rcases j with (⟨⟩ | ⟨⟨⟩⟩) <;> rfl))
  (by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f <;> dsimp <;> simp)

Natural isomorphism between a functor and its associated cospan

Informal description

For any functor $F$ from the walking cospan category to a category $\mathcal{C}$, there is a natural isomorphism between $F$ and the cospan functor constructed from the images of the left and right inclusion morphisms under $F$. Specifically, $F$ is isomorphic to $\mathrm{cospan}\, (F(\mathrm{inl}))\, (F(\mathrm{inr}))$, where $\mathrm{inl}$ and $\mathrm{inr}$ are the left and right inclusion morphisms in the walking cospan category.

CategoryTheory.Limits.diagramIsoSpan definition

(F : WalkingSpan ⥤ C) : F ≅ span (F.map fst) (F.map snd)

Full source

/-- Every diagram indexing a pushout is naturally isomorphic (actually, equal) to a `span` -/
-- @[simps (config := { rhsMd := semireducible })]  Porting note: no semireducible
@[simps!]
def diagramIsoSpan (F : WalkingSpanWalkingSpan ⥤ C) : F ≅ span (F.map fst) (F.map snd) :=
  NatIso.ofComponents
  (fun j => eqToIso (by rcases j with (⟨⟩ | ⟨⟨⟩⟩) <;> rfl))
  (by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f <;> dsimp <;> simp)

Natural isomorphism between a functor and its associated span

Informal description

For any functor $F$ from the walking span category to a category $\mathcal{C}$, there is a natural isomorphism between $F$ and the span functor constructed from the images of the first and second projection morphisms under $F$. Specifically, $F$ is isomorphic to $\mathrm{span}\, (F(\mathrm{fst}))\, (F(\mathrm{snd}))$, where $\mathrm{fst}$ and $\mathrm{snd}$ are the projection morphisms from the apex to the left and right objects in the walking span category.

CategoryTheory.Limits.cospanCompIso definition

(F : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : cospan f g ⋙ F ≅ cospan (F.map f) (F.map g)

Full source

/-- A functor applied to a cospan is a cospan. -/
def cospanCompIso (F : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    cospancospan f g ⋙ Fcospan f g ⋙ F ≅ cospan (F.map f) (F.map g) :=
  NatIso.ofComponents (by rintro (⟨⟩ | ⟨⟨⟩⟩) <;> exact Iso.refl _)
    (by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f <;> dsimp <;> simp)

Natural isomorphism between cospan functor compositions

Informal description

Given a functor $F : C \to D$ and morphisms $f : X \to Z$, $g : Y \to Z$ in $C$, the composition of the cospan functor `cospan f g` with $F$ is naturally isomorphic to the cospan functor `cospan (F.map f) (F.map g)` in $D$.

CategoryTheory.Limits.cospanCompIso_app_left theorem

: (cospanCompIso F f g).app WalkingCospan.left = Iso.refl _

Full source

@[simp]
theorem cospanCompIso_app_left : (cospanCompIso F f g).app WalkingCospan.left = Iso.refl _ := rfl

Identity Component of Cospan Composition Natural Isomorphism at Left Object

Informal description

For a functor $F \colon C \to D$ and morphisms $f \colon X \to Z$, $g \colon Y \to Z$ in $C$, the component of the natural isomorphism $\mathrm{cospanCompIso}\, F\, f\, g$ at the left object of the walking cospan category is equal to the identity isomorphism on $F(X)$.

CategoryTheory.Limits.cospanCompIso_app_right theorem

: (cospanCompIso F f g).app WalkingCospan.right = Iso.refl _

Full source

@[simp]
theorem cospanCompIso_app_right : (cospanCompIso F f g).app WalkingCospan.right = Iso.refl _ :=
  rfl

Identity Component of Cospan Composition Natural Isomorphism at Right Object

Informal description

For a functor $F \colon C \to D$ and morphisms $f \colon X \to Z$, $g \colon Y \to Z$ in $C$, the component of the natural isomorphism $\text{cospanCompIso}\, F\, f\, g$ at the right object of the walking cospan category is equal to the identity isomorphism on $F(Y)$.

CategoryTheory.Limits.cospanCompIso_app_one theorem

: (cospanCompIso F f g).app WalkingCospan.one = Iso.refl _

Full source

@[simp]
theorem cospanCompIso_app_one : (cospanCompIso F f g).app WalkingCospan.one = Iso.refl _ := rfl

Identity Component of Cospan Composition Natural Isomorphism at Central Object

Informal description

For a functor $F \colon C \to D$ and morphisms $f \colon X \to Z$, $g \colon Y \to Z$ in $C$, the component of the natural isomorphism $\text{cospanCompIso}\, F\, f\, g$ at the central object of the walking cospan category is equal to the identity isomorphism on $F(Z)$.

CategoryTheory.Limits.cospanCompIso_hom_app_left theorem

: (cospanCompIso F f g).hom.app WalkingCospan.left = 𝟙 _

Full source

@[simp]
theorem cospanCompIso_hom_app_left : (cospanCompIso F f g).hom.app WalkingCospan.left = 𝟙 _ :=
  rfl

Natural isomorphism component at left object is identity

Informal description

For a functor $F : C \to D$ and morphisms $f : X \to Z$, $g : Y \to Z$ in $C$, the component of the natural isomorphism $(cospanCompIso\, F\, f\, g).hom$ at the left object of the walking cospan category is equal to the identity morphism on $F(X)$.

CategoryTheory.Limits.cospanCompIso_hom_app_right theorem

: (cospanCompIso F f g).hom.app WalkingCospan.right = 𝟙 _

Full source

@[simp]
theorem cospanCompIso_hom_app_right : (cospanCompIso F f g).hom.app WalkingCospan.right = 𝟙 _ :=
  rfl

Identity Component of Cospan Composition Natural Isomorphism at Right Object

Informal description

For a functor $F \colon C \to D$ and morphisms $f \colon X \to Z$, $g \colon Y \to Z$ in $C$, the component of the natural isomorphism $(cospanCompIso\, F\, f\, g).hom$ at the right object of the walking cospan category is equal to the identity morphism on $F(Y)$.

CategoryTheory.Limits.cospanCompIso_hom_app_one theorem

: (cospanCompIso F f g).hom.app WalkingCospan.one = 𝟙 _

Full source

@[simp]
theorem cospanCompIso_hom_app_one : (cospanCompIso F f g).hom.app WalkingCospan.one = 𝟙 _ := rfl

Identity Component of Cospan Composition Natural Isomorphism at Central Object

Informal description

For a functor $F \colon C \to D$ and morphisms $f \colon X \to Z$, $g \colon Y \to Z$ in $C$, the component of the natural isomorphism $(cospanCompIso\, F\, f\, g).hom$ at the central object of the walking cospan category is equal to the identity morphism on $F(Z)$.

CategoryTheory.Limits.cospanCompIso_inv_app_left theorem

: (cospanCompIso F f g).inv.app WalkingCospan.left = 𝟙 _

Full source

@[simp]
theorem cospanCompIso_inv_app_left : (cospanCompIso F f g).inv.app WalkingCospan.left = 𝟙 _ :=
  rfl

Inverse of Cospan Composition Isomorphism at Left Object is Identity

Informal description

For a functor $F \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Z$, $g \colon Y \to Z$ in $\mathcal{C}$, the component of the inverse natural isomorphism $(cospanCompIso\, F\, f\, g).inv$ at the left object of the walking cospan is the identity morphism.

CategoryTheory.Limits.cospanCompIso_inv_app_right theorem

: (cospanCompIso F f g).inv.app WalkingCospan.right = 𝟙 _

Full source

@[simp]
theorem cospanCompIso_inv_app_right : (cospanCompIso F f g).inv.app WalkingCospan.right = 𝟙 _ :=
  rfl

Inverse of Cospan Composition Isomorphism at Right Object is Identity

Informal description

For a functor $F : \mathcal{C} \to \mathcal{D}$ and morphisms $f : X \to Z$, $g : Y \to Z$ in $\mathcal{C}$, the component of the inverse natural isomorphism $(cospanCompIso\, F\, f\, g).inv$ at the right object of the walking cospan is the identity morphism.

CategoryTheory.Limits.cospanCompIso_inv_app_one theorem

: (cospanCompIso F f g).inv.app WalkingCospan.one = 𝟙 _

Full source

@[simp]
theorem cospanCompIso_inv_app_one : (cospanCompIso F f g).inv.app WalkingCospan.one = 𝟙 _ := rfl

Inverse of Cospan Composition Isomorphism at Central Object is Identity

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Z$, $g \colon Y \to Z$ in $\mathcal{C}$, the component of the inverse natural isomorphism $(cospanCompIso\, F\, f\, g).inv$ at the central object of the walking cospan is the identity morphism.

CategoryTheory.Limits.spanCompIso definition

(F : C ⥤ D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : span f g ⋙ F ≅ span (F.map f) (F.map g)

Full source

/-- A functor applied to a span is a span. -/
def spanCompIso (F : C ⥤ D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) :
    spanspan f g ⋙ Fspan f g ⋙ F ≅ span (F.map f) (F.map g) :=
  NatIso.ofComponents (by rintro (⟨⟩ | ⟨⟨⟩⟩) <;> exact Iso.refl _)
    (by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f <;> dsimp <;> simp)

Natural isomorphism between post-composed span and span of post-composed morphisms

Informal description

Given a functor $F : \mathcal{C} \to \mathcal{D}$ and morphisms $f : X \to Y$, $g : X \to Z$ in $\mathcal{C}$, there is a natural isomorphism between the functors obtained by first constructing the span $(f, g)$ in $\mathcal{C}$ and then applying $F$, and constructing the span $(F(f), F(g))$ directly in $\mathcal{D}$. More precisely, the isomorphism relates: - The composition of the span functor $\text{span}\, f\, g : \text{WalkingSpan} \to \mathcal{C}$ with $F$ - The span functor $\text{span}\, (F \circ f)\, (F \circ g) : \text{WalkingSpan} \to \mathcal{D}$

CategoryTheory.Limits.spanCompIso_app_left theorem

: (spanCompIso F f g).app WalkingSpan.left = Iso.refl _

Full source

@[simp]
theorem spanCompIso_app_left : (spanCompIso F f g).app WalkingSpan.left = Iso.refl _ := rfl

Left Component of Span Post-Composition Isomorphism is Identity

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Y$, $g \colon X \to Z$ in $\mathcal{C}$, the component of the natural isomorphism $\text{spanCompIso}\, F\, f\, g$ at the left object of the walking span is the identity isomorphism.

CategoryTheory.Limits.spanCompIso_app_right theorem

: (spanCompIso F f g).app WalkingSpan.right = Iso.refl _

Full source

@[simp]
theorem spanCompIso_app_right : (spanCompIso F f g).app WalkingSpan.right = Iso.refl _ := rfl

Right Component of Span Post-Composition Isomorphism is Identity

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Y$, $g \colon X \to Z$ in $\mathcal{C}$, the component of the natural isomorphism $\text{spanCompIso}\, F\, f\, g$ at the right object of the walking span is the identity isomorphism.

CategoryTheory.Limits.spanCompIso_app_zero theorem

: (spanCompIso F f g).app WalkingSpan.zero = Iso.refl _

Full source

@[simp]
theorem spanCompIso_app_zero : (spanCompIso F f g).app WalkingSpan.zero = Iso.refl _ := rfl

Apex Component of Span Post-Composition Isomorphism is Identity

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Y$, $g \colon X \to Z$ in $\mathcal{C}$, the component of the natural isomorphism $\text{spanCompIso}\, F\, f\, g$ at the apex object (zero) of the walking span is the identity isomorphism.

CategoryTheory.Limits.spanCompIso_hom_app_left theorem

: (spanCompIso F f g).hom.app WalkingSpan.left = 𝟙 _

Full source

@[simp]
theorem spanCompIso_hom_app_left : (spanCompIso F f g).hom.app WalkingSpan.left = 𝟙 _ := rfl

Left Component of Span Post-Composition Isomorphism Homomorphism is Identity

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Y$, $g \colon X \to Z$ in $\mathcal{C}$, the left component of the homomorphism part of the natural isomorphism $\text{spanCompIso}\, F\, f\, g$ is the identity morphism on $F(Y)$.

CategoryTheory.Limits.spanCompIso_hom_app_right theorem

: (spanCompIso F f g).hom.app WalkingSpan.right = 𝟙 _

Full source

@[simp]
theorem spanCompIso_hom_app_right : (spanCompIso F f g).hom.app WalkingSpan.right = 𝟙 _ := rfl

Right Component of Span Post-Composition Isomorphism Homomorphism is Identity

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Y$, $g \colon X \to Z$ in $\mathcal{C}$, the right component of the homomorphism part of the natural isomorphism $\text{spanCompIso}\, F\, f\, g$ is the identity morphism on $F(Z)$.

CategoryTheory.Limits.spanCompIso_hom_app_zero theorem

: (spanCompIso F f g).hom.app WalkingSpan.zero = 𝟙 _

Full source

@[simp]
theorem spanCompIso_hom_app_zero : (spanCompIso F f g).hom.app WalkingSpan.zero = 𝟙 _ := rfl

Apex Component of Span Post-Composition Isomorphism Homomorphism is Identity

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ and morphisms $f \colon X \to Y$, $g \colon X \to Z$ in $\mathcal{C}$, the component of the homomorphism part of the natural isomorphism $\text{spanCompIso}\, F\, f\, g$ at the apex object (zero) of the walking span category is the identity morphism on $F(X)$.

CategoryTheory.Limits.spanCompIso_inv_app_left theorem

: (spanCompIso F f g).inv.app WalkingSpan.left = 𝟙 _

Full source

@[simp]
theorem spanCompIso_inv_app_left : (spanCompIso F f g).inv.app WalkingSpan.left = 𝟙 _ := rfl

Inverse of Span Composition Isomorphism Acts as Identity on Left Object

Informal description

For a functor $F : \mathcal{C} \to \mathcal{D}$ and morphisms $f : X \to Y$, $g : X \to Z$ in $\mathcal{C}$, the component of the inverse of the natural isomorphism $\text{spanCompIso}\, F\, f\, g$ at the left object of the walking span category is the identity morphism. In other words, the inverse of the isomorphism between the post-composed span functor and the span of post-composed morphisms acts as the identity on the left object.

CategoryTheory.Limits.spanCompIso_inv_app_right theorem

: (spanCompIso F f g).inv.app WalkingSpan.right = 𝟙 _

Full source

@[simp]
theorem spanCompIso_inv_app_right : (spanCompIso F f g).inv.app WalkingSpan.right = 𝟙 _ := rfl

Identity Action of Span Composition Isomorphism Inverse on Right Object

Informal description

For a functor $F : \mathcal{C} \to \mathcal{D}$ and morphisms $f : X \to Y$, $g : X \to Z$ in $\mathcal{C}$, the component of the inverse of the natural isomorphism $\text{spanCompIso}\, F\, f\, g$ at the right object of the walking span category is the identity morphism. In other words, the inverse of the isomorphism between the post-composed span functor and the span of post-composed morphisms acts as the identity on the right object.

CategoryTheory.Limits.spanCompIso_inv_app_zero theorem

: (spanCompIso F f g).inv.app WalkingSpan.zero = 𝟙 _

Full source

@[simp]
theorem spanCompIso_inv_app_zero : (spanCompIso F f g).inv.app WalkingSpan.zero = 𝟙 _ := rfl

Identity Action of Span Composition Isomorphism Inverse on Apex Object

Informal description

For a functor $F : \mathcal{C} \to \mathcal{D}$ and morphisms $f : X \to Y$, $g : X \to Z$ in $\mathcal{C}$, the component of the inverse of the natural isomorphism $\text{spanCompIso}\, F\, f\, g$ at the apex object (zero) of the walking span category is the identity morphism.

CategoryTheory.Limits.cospanExt definition

(wf : iX.hom ≫ f' = f ≫ iZ.hom) (wg : iY.hom ≫ g' = g ≫ iZ.hom) : cospan f g ≅ cospan f' g'

Full source

/-- Construct an isomorphism of cospans from components. -/
def cospanExt (wf : iX.hom ≫ f' = f ≫ iZ.hom) (wg : iY.hom ≫ g' = g ≫ iZ.hom) :
    cospancospan f g ≅ cospan f' g' :=
  NatIso.ofComponents
    (by rintro (⟨⟩ | ⟨⟨⟩⟩); exacts [iZ, iX, iY])
    (by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f <;> dsimp <;> simp [wf, wg])

Isomorphism of cospan diagrams from component isomorphisms

Informal description

Given isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f : X \to Z$, $f' : X' \to Z'$, $g : Y \to Z$, $g' : Y' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Z$ and $i_Y \circ g' = g \circ i_Z$), this constructs an isomorphism between the cospan diagrams $(f,g)$ and $(f',g')$.

CategoryTheory.Limits.cospanExt_app_left theorem

: (cospanExt iX iY iZ wf wg).app WalkingCospan.left = iX

Full source

@[simp]
theorem cospanExt_app_left : (cospanExt iX iY iZ wf wg).app WalkingCospan.left = iX := by
  dsimp [cospanExt]

Left Component of Cospan Diagram Isomorphism

Informal description

Given isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f : X \to Z$, $f' : X' \to Z'$, $g : Y \to Z$, $g' : Y' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Z$ and $i_Y \circ g' = g \circ i_Z$), the component of the induced isomorphism $(cospanExt\ i_X\ i_Y\ i_Z\ wf\ wg)$ at the left object of the walking cospan equals $i_X$.

CategoryTheory.Limits.cospanExt_app_right theorem

: (cospanExt iX iY iZ wf wg).app WalkingCospan.right = iY

Full source

@[simp]
theorem cospanExt_app_right : (cospanExt iX iY iZ wf wg).app WalkingCospan.right = iY := by
  dsimp [cospanExt]

Right Component of Cospan Diagram Isomorphism

Informal description

Given isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f : X \to Z$, $f' : X' \to Z'$, $g : Y \to Z$, $g' : Y' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Z$ and $i_Y \circ g' = g \circ i_Z$), the component of the induced isomorphism $(cospanExt\ i_X\ i_Y\ i_Z\ wf\ wg)$ at the right object of the walking cospan equals $i_Y$.

CategoryTheory.Limits.cospanExt_app_one theorem

: (cospanExt iX iY iZ wf wg).app WalkingCospan.one = iZ

Full source

@[simp]
theorem cospanExt_app_one : (cospanExt iX iY iZ wf wg).app WalkingCospan.one = iZ := by
  dsimp [cospanExt]

Central Component of Cospan Diagram Isomorphism

Informal description

Given isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f : X \to Z$, $f' : X' \to Z'$, $g : Y \to Z$, $g' : Y' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Z$ and $i_Y \circ g' = g \circ i_Z$), the component of the induced isomorphism $(cospanExt\ i_X\ i_Y\ i_Z\ wf\ wg)$ at the central object of the walking cospan equals $i_Z$.

CategoryTheory.Limits.cospanExt_hom_app_left theorem

: (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.left = iX.hom

Full source

@[simp]
theorem cospanExt_hom_app_left :
    (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.left = iX.hom := by dsimp [cospanExt]

Left Component of Cospan Diagram Isomorphism Homomorphism

Informal description

Given isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f : X \to Z$, $f' : X' \to Z'$, $g : Y \to Z$, $g' : Y' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Z$ and $i_Y \circ g' = g \circ i_Z$), the left component of the homomorphism part of the induced isomorphism $(cospanExt\ i_X\ i_Y\ i_Z\ wf\ wg)$ equals the homomorphism part of $i_X$.

CategoryTheory.Limits.cospanExt_hom_app_right theorem

: (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.right = iY.hom

Full source

@[simp]
theorem cospanExt_hom_app_right :
    (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.right = iY.hom := by dsimp [cospanExt]

Right Component of Cospan Diagram Isomorphism Homomorphism

Informal description

Given isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f : X \to Z$, $f' : X' \to Z'$, $g : Y \to Z$, $g' : Y' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Z$ and $i_Y \circ g' = g \circ i_Z$), the right component of the homomorphism part of the induced isomorphism $(cospanExt\ i_X\ i_Y\ i_Z\ wf\ wg)$ equals the homomorphism part of $i_Y$.

CategoryTheory.Limits.cospanExt_hom_app_one theorem

: (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.one = iZ.hom

Full source

@[simp]
theorem cospanExt_hom_app_one : (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.one = iZ.hom := by
  dsimp [cospanExt]

Central Component of Cospan Diagram Isomorphism Homomorphism

Informal description

Given isomorphisms $i_X \colon X \to X'$, $i_Y \colon Y \to Y'$, and $i_Z \colon Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f \colon X \to Z$, $f' \colon X' \to Z'$, $g \colon Y \to Z$, $g' \colon Y' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Z$ and $i_Y \circ g' = g \circ i_Z$), the component of the homomorphism part of the induced isomorphism $(cospanExt\ i_X\ i_Y\ i_Z\ wf\ wg)$ at the central object of the walking cospan equals the homomorphism part of $i_Z$.

CategoryTheory.Limits.cospanExt_inv_app_left theorem

: (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.left = iX.inv

Full source

@[simp]
theorem cospanExt_inv_app_left :
    (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.left = iX.inv := by dsimp [cospanExt]

Inverse of Cospan Isomorphism at Left Object Equals Inverse of Left Component Isomorphism

Informal description

Given isomorphisms $i_X \colon X \to X'$, $i_Y \colon Y \to Y'$, and $i_Z \colon Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f \colon X \to Z$, $f' \colon X' \to Z'$, $g \colon Y \to Z$, $g' \colon Y' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Z$ and $i_Y \circ g' = g \circ i_Z$), the inverse of the natural isomorphism between the cospan diagrams $(f,g)$ and $(f',g')$, when evaluated at the left object of the walking cospan, equals the inverse of $i_X$.

CategoryTheory.Limits.cospanExt_inv_app_right theorem

: (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.right = iY.inv

Full source

@[simp]
theorem cospanExt_inv_app_right :
    (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.right = iY.inv := by dsimp [cospanExt]

Inverse of Cospan Isomorphism at Right Object Equals Inverse of Right Component Isomorphism

Informal description

For isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$ and morphisms $f : X \to Z$, $f' : X' \to Z'$, $g : Y \to Z$, $g' : Y' \to Z'$ satisfying the commuting conditions $i_X \circ f' = f \circ i_Z$ and $i_Y \circ g' = g \circ i_Z$, the inverse of the natural isomorphism between the cospan diagrams $(f,g)$ and $(f',g')$, when evaluated at the right object of the walking cospan, equals the inverse of $i_Y$.

CategoryTheory.Limits.cospanExt_inv_app_one theorem

: (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.one = iZ.inv

Full source

@[simp]
theorem cospanExt_inv_app_one : (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.one = iZ.inv := by
  dsimp [cospanExt]

Inverse of Cospan Isomorphism at Central Object Equals Inverse of Central Component Isomorphism

Informal description

For isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$ and morphisms $f : X \to Z$, $f' : X' \to Z'$, $g : Y \to Z$, $g' : Y' \to Z'$ satisfying the commuting conditions $i_X \circ f' = f \circ i_Z$ and $i_Y \circ g' = g \circ i_Z$, the inverse of the natural isomorphism between the cospan diagrams $(f,g)$ and $(f',g')$, when evaluated at the central object of the walking cospan, equals the inverse of $i_Z$.

CategoryTheory.Limits.spanExt definition

(wf : iX.hom ≫ f' = f ≫ iY.hom) (wg : iX.hom ≫ g' = g ≫ iZ.hom) : span f g ≅ span f' g'

Full source

/-- Construct an isomorphism of spans from components. -/
def spanExt (wf : iX.hom ≫ f' = f ≫ iY.hom) (wg : iX.hom ≫ g' = g ≫ iZ.hom) :
    spanspan f g ≅ span f' g' :=
  NatIso.ofComponents (by rintro (⟨⟩ | ⟨⟨⟩⟩); exacts [iX, iY, iZ])
    (by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f <;> cases f <;> dsimp <;> simp [wf, wg])

Isomorphism of spans from commuting squares

Informal description

Given isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f : X \to Y$, $g : X \to Z$, $f' : X' \to Y'$, $g' : X' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Y$ and $i_X \circ g' = g \circ i_Z$), this constructs an isomorphism between the span functors $\text{span}\, f\, g$ and $\text{span}\, f'\, g'$.

CategoryTheory.Limits.spanExt_app_left theorem

: (spanExt iX iY iZ wf wg).app WalkingSpan.left = iY

Full source

@[simp]
theorem spanExt_app_left : (spanExt iX iY iZ wf wg).app WalkingSpan.left = iY := by
  dsimp [spanExt]

Left Component of Span Isomorphism Equals $i_Y$

Informal description

Given isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f : X \to Y$, $g : X \to Z$, $f' : X' \to Y'$, $g' : X' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Y$ and $i_X \circ g' = g \circ i_Z$), the component of the isomorphism $\text{span}\, f\, g \cong \text{span}\, f'\, g'$ at the left object of the walking span is equal to $i_Y$.

CategoryTheory.Limits.spanExt_app_right theorem

: (spanExt iX iY iZ wf wg).app WalkingSpan.right = iZ

Full source

@[simp]
theorem spanExt_app_right : (spanExt iX iY iZ wf wg).app WalkingSpan.right = iZ := by
  dsimp [spanExt]

Right Component of Span Isomorphism

Informal description

For isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f : X \to Y$, $g : X \to Z$, $f' : X' \to Y'$, $g' : X' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Y$ and $i_X \circ g' = g \circ i_Z$), the component of the isomorphism $\text{span}\, f\, g \cong \text{span}\, f'\, g'$ at the right object of the walking span is equal to $i_Z$.

CategoryTheory.Limits.spanExt_app_one theorem

: (spanExt iX iY iZ wf wg).app WalkingSpan.zero = iX

Full source

@[simp]
theorem spanExt_app_one : (spanExt iX iY iZ wf wg).app WalkingSpan.zero = iX := by
  dsimp [spanExt]

Apex Component of Span Isomorphism Equals $i_X$

Informal description

Given isomorphisms $i_X \colon X \to X'$, $i_Y \colon Y \to Y'$, $i_Z \colon Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f \colon X \to Y$, $g \colon X \to Z$, $f' \colon X' \to Y'$, $g' \colon X' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Y$ and $i_X \circ g' = g \circ i_Z$), the component of the isomorphism $\text{span}\, f\, g \cong \text{span}\, f'\, g'$ at the apex (zero object) of the walking span is equal to $i_X$.

CategoryTheory.Limits.spanExt_hom_app_left theorem

: (spanExt iX iY iZ wf wg).hom.app WalkingSpan.left = iY.hom

Full source

@[simp]
theorem spanExt_hom_app_left : (spanExt iX iY iZ wf wg).hom.app WalkingSpan.left = iY.hom := by
  dsimp [spanExt]

Left Component of Span Isomorphism Homomorphism

Informal description

For isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f : X \to Y$, $g : X \to Z$, $f' : X' \to Y'$, $g' : X' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Y$ and $i_X \circ g' = g \circ i_Z$), the left component of the homomorphism of the isomorphism $\text{span}\, f\, g \cong \text{span}\, f'\, g'$ is equal to the morphism $i_Y$.

CategoryTheory.Limits.spanExt_hom_app_right theorem

: (spanExt iX iY iZ wf wg).hom.app WalkingSpan.right = iZ.hom

Full source

@[simp]
theorem spanExt_hom_app_right : (spanExt iX iY iZ wf wg).hom.app WalkingSpan.right = iZ.hom := by
  dsimp [spanExt]

Right Component of Span Isomorphism Homomorphism Equals $i_Z$

Informal description

Given isomorphisms $i_X \colon X \to X'$, $i_Y \colon Y \to Y'$, $i_Z \colon Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f \colon X \to Y$, $g \colon X \to Z$, $f' \colon X' \to Y'$, $g' \colon X' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Y$ and $i_X \circ g' = g \circ i_Z$), the right component of the homomorphism of the isomorphism $\text{span}\, f\, g \cong \text{span}\, f'\, g'$ is equal to the morphism $i_Z$.

CategoryTheory.Limits.spanExt_hom_app_zero theorem

: (spanExt iX iY iZ wf wg).hom.app WalkingSpan.zero = iX.hom

Full source

@[simp]
theorem spanExt_hom_app_zero : (spanExt iX iY iZ wf wg).hom.app WalkingSpan.zero = iX.hom := by
  dsimp [spanExt]

Apex Component of Span Isomorphism Homomorphism

Informal description

Given isomorphisms $i_X \colon X \to X'$, $i_Y \colon Y \to Y'$, $i_Z \colon Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f \colon X \to Y$, $g \colon X \to Z$, $f' \colon X' \to Y'$, $g' \colon X' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Y$ and $i_X \circ g' = g \circ i_Z$), the component of the isomorphism $\text{span}\, f\, g \cong \text{span}\, f'\, g'$ at the apex (zero object) of the walking span is equal to the morphism $i_X$.

CategoryTheory.Limits.spanExt_inv_app_left theorem

: (spanExt iX iY iZ wf wg).inv.app WalkingSpan.left = iY.inv

Full source

@[simp]
theorem spanExt_inv_app_left : (spanExt iX iY iZ wf wg).inv.app WalkingSpan.left = iY.inv := by
  dsimp [spanExt]

Inverse of Span Isomorphism at Left Object Equals Inverse Morphism

Informal description

For isomorphisms $i_X \colon X \to X'$, $i_Y \colon Y \to Y'$, $i_Z \colon Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f \colon X \to Y$, $g \colon X \to Z$, $f' \colon X' \to Y'$, $g' \colon X' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Y$ and $i_X \circ g' = g \circ i_Z$), the component of the inverse of the span isomorphism at the left object of the walking span is equal to the inverse morphism $i_Y^{-1} \colon Y' \to Y$.

CategoryTheory.Limits.spanExt_inv_app_right theorem

: (spanExt iX iY iZ wf wg).inv.app WalkingSpan.right = iZ.inv

Full source

@[simp]
theorem spanExt_inv_app_right : (spanExt iX iY iZ wf wg).inv.app WalkingSpan.right = iZ.inv := by
  dsimp [spanExt]

Inverse of Span Isomorphism at Right Object Equals Inverse Morphism

Informal description

For isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f : X \to Y$, $g : X \to Z$, $f' : X' \to Y'$, $g' : X' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Y$ and $i_X \circ g' = g \circ i_Z$), the component of the inverse of the span isomorphism at the right object of the walking span is equal to the inverse morphism $i_Z^{-1} : Z' \to Z$.

CategoryTheory.Limits.spanExt_inv_app_zero theorem

: (spanExt iX iY iZ wf wg).inv.app WalkingSpan.zero = iX.inv

Full source

@[simp]
theorem spanExt_inv_app_zero : (spanExt iX iY iZ wf wg).inv.app WalkingSpan.zero = iX.inv := by
  dsimp [spanExt]

Inverse Span Isomorphism at Apex Equals Inverse Morphism

Informal description

For isomorphisms $i_X : X \to X'$, $i_Y : Y \to Y'$, $i_Z : Z \to Z'$ in a category $\mathcal{C}$, and morphisms $f : X \to Y$, $g : X \to Z$, $f' : X' \to Y'$, $g' : X' \to Z'$ such that the diagrams commute ($i_X \circ f' = f \circ i_Y$ and $i_X \circ g' = g \circ i_Z$), the component of the inverse of the span isomorphism at the apex object (zero) of the walking span is equal to the inverse morphism $i_X^{-1} : X' \to X$.

References