English
There is a canonical bijection between the sections of a multicospan index I and the sections of its multicospan, i.e., I.sections ≃ I.multicospan.sections.Elem.
Русский
Существует каноническое биекционное соответствие между секциями индекса мультисовпавшего графа I и секциями его мультисовпана, то есть I.sections ≃ I.multicospan.sections.Elem.
LaTeX
$$$I.sections \\cong I.multicospan.sections.Elem$$$
Lean4
/-- The bijection `I.sections ≃ I.multicospan.sections` when `I : MulticospanIndex (Type u)`
is a multiequalizer diagram in the category of types. -/
@[simps]
def sectionsEquiv : I.sections ≃ I.multicospan.sections
where
toFun
s :=
{ val := fun i ↦
match i with
| .left i => s.val i
| .right j => I.fst j (s.val _)
property := by
rintro _ _ (_ | _ | r)
· rfl
· rfl
· exact (s.property r).symm }
invFun
s :=
{ val := fun i ↦ s.val (.left i)
property := fun r ↦ (s.property (.fst r)).trans (s.property (.snd r)).symm }
right_inv
s := by
ext (_ | r)
· rfl
· exact s.property (.fst r)
