Bicategories of spans in a category

In this file, given a category C and two morphism properties Wₗ and Wᵣ in C that are stable under compositions, contain identities and such that for any morphism b : x₃ ⟶ x₄ in Wₗ and any morphism r : x₂ → x₃ in Wᵣ, there exists a pullback square

     t
  x₁ --> x₂
  |      |
l |      | r
  v      v
  x₃ --> x₄
     b

in C such that t satisfies Wₗ and l satisfies Wᵣ, we construct the bicategory of spans in C with left morphism in Wₗ and right morphism in Wᵣ (TODO @robin-carlier).

structure CategoryTheory.Span {C : Type u_1} [Category.{v_1, u_1} C] (Wₗ Wᵣ : MorphismProperty C) (c c' : C) : Type (max u_1 v_1)

A (Wₗ, Wᵣ)-span from c to c' is the data of an object a : C, together with a morphism a ⟶ c in Wₗ, and a morphism a ⟶ c' in Wᵣ.

• apex : C

  the apex of the span

• l : self.apex ⟶ c

  the left map

• r : self.apex ⟶ c'

  the right map

• wl : Wₗ self.l
• wr : Wᵣ self.r

structure CategoryTheory.Span.Hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} (S₁ S₂ : Span Wₗ Wᵣ c c') : Type v_1

A morphism of spans is a morphism between the apices compatible with the projections.

• hom : S₁.apex ⟶ S₂.apex

  the map between the apices

• hom_l : CategoryStruct.comp self.hom S₂.l = S₁.l
• hom_r : CategoryStruct.comp self.hom S₂.r = S₁.r

@[simp]

theorem CategoryTheory.Span.Hom.hom_r_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S₁ S₂ : Span Wₗ Wᵣ c c'} (self : S₁.Hom S₂) {Z : C} (h : c' ⟶ Z) : CategoryStruct.comp self.hom (CategoryStruct.comp S₂.r h) = CategoryStruct.comp S₁.r h

@[simp]

theorem CategoryTheory.Span.Hom.hom_l_assoc {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S₁ S₂ : Span Wₗ Wᵣ c c'} (self : S₁.Hom S₂) {Z : C} (h : c ⟶ Z) : CategoryStruct.comp self.hom (CategoryStruct.comp S₂.l h) = CategoryStruct.comp S₁.l h

@[implicit_reducible]

instance CategoryTheory.Span.instCategory {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} : Category.{v_1, max u_1 v_1} (Span Wₗ Wᵣ c c')

Equations

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

@[simp]

theorem CategoryTheory.Span.id_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} (S : Span Wₗ Wᵣ c c') : (CategoryStruct.id S).hom = CategoryStruct.id S.apex

@[simp]

theorem CategoryTheory.Span.comp_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {X✝ Y✝ Z✝ : Span Wₗ Wᵣ c c'} (φ : X✝.Hom Y✝) (φ' : Y✝.Hom Z✝) : (CategoryStruct.comp φ φ').hom = CategoryStruct.comp φ.hom φ'.hom

theorem CategoryTheory.Span.hom_ext {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S S' : Span Wₗ Wᵣ c c'} {f g : S ⟶ S'} (h : f.hom = g.hom) : f = g

theorem CategoryTheory.Span.hom_ext_iff {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S S' : Span Wₗ Wᵣ c c'} {f g : S ⟶ S'} : f = g ↔ f.hom = g.hom

def CategoryTheory.Span.mkIso {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S S' : Span Wₗ Wᵣ c c'} (e : S.apex ≅ S'.apex) (hₗ : CategoryStruct.comp e.hom S'.l = S.l := by cat_disch) (hᵣ : CategoryStruct.comp e.hom S'.r = S.r := by cat_disch) : S ≅ S'

Construct an isomorphism of spans from an isomorphism between the apices that is compatible with the projections.

Equations

• CategoryTheory.Span.mkIso e hₗ hᵣ = { hom := { hom := e.hom, hom_l := ⋯, hom_r := ⋯ }, inv := { hom := e.inv, hom_l := ⋯, hom_r := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Span.mkIso_inv_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S S' : Span Wₗ Wᵣ c c'} (e : S.apex ≅ S'.apex) (hₗ : CategoryStruct.comp e.hom S'.l = S.l := by cat_disch) (hᵣ : CategoryStruct.comp e.hom S'.r = S.r := by cat_disch) : (mkIso e hₗ hᵣ).inv.hom = e.inv

@[simp]

theorem CategoryTheory.Span.mkIso_hom_hom {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} {S S' : Span Wₗ Wᵣ c c'} (e : S.apex ≅ S'.apex) (hₗ : CategoryStruct.comp e.hom S'.l = S.l := by cat_disch) (hᵣ : CategoryStruct.comp e.hom S'.r = S.r := by cat_disch) : (mkIso e hₗ hᵣ).hom.hom = e.hom

instance CategoryTheory.Span.instHasPullbackRL {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.HasPullbacksAgainst Wᵣ] {c c' c'' : C} (S₁ : Span Wₗ Wᵣ c c') (S₂ : Span Wₗ Wᵣ c' c'') : Limits.HasPullback S₁.r S₂.l

instance CategoryTheory.Span.instIsStableUnderBaseChangeAlongR {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] (S₁ : Span Wₗ Wᵣ c c') : Wₗ.IsStableUnderBaseChangeAlong S₁.r

instance CategoryTheory.Span.instIsStableUnderBaseChangeAlongL {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} {c c' : C} [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] (S₁ : Span Wₗ Wᵣ c c') : Wᵣ.IsStableUnderBaseChangeAlong S₁.l

def CategoryTheory.Span.id {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] (c : C) : Span Wₗ Wᵣ c c

The identity span, where both legs are identity morphisms.

Equations

• CategoryTheory.Span.id c = { apex := c, l := CategoryTheory.CategoryStruct.id c, r := CategoryTheory.CategoryStruct.id c, wl := ⋯, wr := ⋯ }

@[simp]

theorem CategoryTheory.Span.id_l {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] (c : C) : (id c).l = CategoryStruct.id c

@[simp]

theorem CategoryTheory.Span.id_apex {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] (c : C) : (id c).apex = c

@[simp]

theorem CategoryTheory.Span.id_r {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.ContainsIdentities] [Wᵣ.ContainsIdentities] (c : C) : (id c).r = CategoryStruct.id c

noncomputable def CategoryTheory.Span.comp {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {c c' c'' : C} (S₁ : Span Wₗ Wᵣ c c') (S₂ : Span Wₗ Wᵣ c' c'') : Span Wₗ Wᵣ c c''

The composition of two spans: if the relevant pullback exists and if the morphism properties are stable under the relevant base change, it is given by the total span

     P
    /  \
   /    \
  X₁     X₂
 /  \   /  \
c     c'    c''

where the top diamond is a pullback square

Equations

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

@[simp]

theorem CategoryTheory.Span.comp_apex {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {c c' c'' : C} (S₁ : Span Wₗ Wᵣ c c') (S₂ : Span Wₗ Wᵣ c' c'') : (S₁.comp S₂).apex = Limits.pullback S₁.r S₂.l

@[simp]

theorem CategoryTheory.Span.comp_r {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {c c' c'' : C} (S₁ : Span Wₗ Wᵣ c c') (S₂ : Span Wₗ Wᵣ c' c'') : (S₁.comp S₂).r = CategoryStruct.comp (Limits.pullback.snd S₁.r S₂.l) S₂.r

@[simp]

theorem CategoryTheory.Span.comp_l {C : Type u_1} [Category.{v_1, u_1} C] {Wₗ Wᵣ : MorphismProperty C} [Wₗ.HasPullbacksAgainst Wᵣ] [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [Wₗ.IsStableUnderComposition] [Wᵣ.IsStableUnderComposition] {c c' c'' : C} (S₁ : Span Wₗ Wᵣ c c') (S₂ : Span Wₗ Wᵣ c' c'') : (S₁.comp S₂).l = CategoryStruct.comp (Limits.pullback.fst S₁.r S₂.l) S₁.l