Multiequalizers in Type

Given J : MulticospanShape and I : MulticospanIndex J (Type u), we define a type I.sections. When c : Multifork I, we show that c is a limit iff the canonical map c.toSections : c.pt → I.sections is a bijection.

structure CategoryTheory.Limits.MulticospanIndex.sections {J : MulticospanShape} (I : MulticospanIndex J (Type u)) : Type (max u u_1)

Given I : MulticospanIndex J (Type u), this is a type which identifies to the sections of the functor I.multicospan.

• val (i : J.L) : I.left i

  The data of an element in I.left i for each i : J.L.

• property (r : J.R) : (ConcreteCategory.hom (I.fst r)) (self.val (J.fst r)) = (ConcreteCategory.hom (I.snd r)) (self.val (J.snd r))

theorem CategoryTheory.Limits.MulticospanIndex.sections.ext_iff {J : MulticospanShape} {I : MulticospanIndex J (Type u)} {x y : I.sections} : x = y ↔ x.val = y.val

theorem CategoryTheory.Limits.MulticospanIndex.sections.ext {J : MulticospanShape} {I : MulticospanIndex J (Type u)} {x y : I.sections} (val : x.val = y.val) : x = y

def CategoryTheory.Limits.MulticospanIndex.sectionsEquiv {J : MulticospanShape} (I : MulticospanIndex J (Type u)) : I.sections ≃ ↑I.multicospan.sections

The bijection I.sections ≃ I.multicospan.sections when I : MulticospanIndex (Type u) is a multiequalizer diagram in the category of types.

Equations

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

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.sectionsEquiv_apply_coe {J : MulticospanShape} (I : MulticospanIndex J (Type u)) (s : I.sections) (i : WalkingMulticospan J) : ↑(I.sectionsEquiv s) i = match i with | WalkingMulticospan.left i => s.val i | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j))

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.sectionsEquiv_symm_apply_val {J : MulticospanShape} (I : MulticospanIndex J (Type u)) (s : ↑I.multicospan.sections) (i : J.L) : (I.sectionsEquiv.symm s).val i = ↑s (WalkingMulticospan.left i)

def CategoryTheory.Limits.Multifork.toSections {J : MulticospanShape} {I : MulticospanIndex J (Type u)} (c : Multifork I) (x : c.pt) : I.sections

Given a multiequalizer diagram I : MulticospanIndex (Type u) in the category of types and c a multifork for I, this is the canonical map c.pt → I.sections.

Equations

• c.toSections x = { val := fun (i : J.L) => (CategoryTheory.ConcreteCategory.hom (c.ι i)) x, property := ⋯ }

@[simp]

theorem CategoryTheory.Limits.Multifork.toSections_val {J : MulticospanShape} {I : MulticospanIndex J (Type u)} (c : Multifork I) (x : c.pt) (i : J.L) : (c.toSections x).val i = (ConcreteCategory.hom (c.ι i)) x

theorem CategoryTheory.Limits.Multifork.toSections_fac {J : MulticospanShape} {I : MulticospanIndex J (Type u)} (c : Multifork I) : ⇑I.sectionsEquiv.symm ∘ Types.sectionOfCone c = c.toSections

theorem CategoryTheory.Limits.Multifork.isLimit_types_iff {J : MulticospanShape} {I : MulticospanIndex J (Type u)} (c : Multifork I) : Nonempty (IsLimit c) ↔ Function.Bijective c.toSections

A multifork c : Multifork I in the category of types is limit iff the map c.toSections : c.pt → I.sections is a bijection.

noncomputable def CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv {J : MulticospanShape} {I : MulticospanIndex J (Type u)} {c : Multifork I} (hc : IsLimit c) : I.sections ≃ c.pt

The bijection I.sections ≃ c.pt when c : Multifork I is a limit multifork in the category of types.

Equations

• CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv hc = (Equiv.ofBijective c.toSections ⋯).symm

@[simp]

theorem CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_symm_apply_val {J : MulticospanShape} {I : MulticospanIndex J (Type u)} {c : Multifork I} (hc : IsLimit c) (x : c.pt) (i : J.L) : ((sectionsEquiv hc).symm x).val i = (ConcreteCategory.hom (c.ι i)) x

@[simp]

theorem CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_apply_val {J : MulticospanShape} {I : MulticospanIndex J (Type u)} {c : Multifork I} (hc : IsLimit c) (s : I.sections) (i : J.L) : (ConcreteCategory.hom (c.ι i)) ((sectionsEquiv hc) s) = s.val i