English
For a binary cofan c = (c.inl, c.inr), the colimit property holds if and only if c.inl and c.inr are injective and their ranges are complementary (IsCompl).
Русский
Для бинарного кофана c = (c.inl, c.inr) условие колимита выполняется тогда, когда c.inl и c.inr инъективны и их области_IMAGE являются взаимодополняющими (IsCompl).
LaTeX
$$$$ Nonempty(IsColimit\\, c) \\iff Injective\\, c.inl \\land Injective\\, c.inr \\land IsCompl (\\mathrm{range}\\, c.inl) (\\mathrm{range}\\, c.inr) $$$$
Lean4
theorem binaryCofan_isColimit_iff {X Y : Type u} (c : BinaryCofan X Y) :
Nonempty (IsColimit c) ↔ Injective c.inl ∧ Injective c.inr ∧ IsCompl (Set.range c.inl) (Set.range c.inr) := by
classical
constructor
· rintro ⟨h⟩
rw [← show _ = c.inl from h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.left⟩, ←
show _ = c.inr from h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.right⟩]
dsimp [binaryCoproductCocone]
refine
⟨(h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp Sum.inl_injective,
(h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp Sum.inr_injective, ?_⟩
rw [types_comp, Set.range_comp, ← eq_compl_iff_isCompl, types_comp, Set.range_comp _ Sum.inr]
erw [← Set.image_compl_eq (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.bijective]
simp
· rintro ⟨h₁, h₂, h₃⟩
have : ∀ x, x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr :=
by
rw [eq_compl_iff_isCompl.mpr h₃.symm]
exact fun _ => or_not
refine ⟨BinaryCofan.IsColimit.mk _ ?_ ?_ ?_ ?_⟩
· intro T f g x
exact
if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective _ h₁).symm ⟨x, h⟩)
else g ((Equiv.ofInjective _ h₂).symm ⟨x, (this x).resolve_left h⟩)
· intro T f g
funext x
simp [h₁.eq_iff]
· intro T f g
funext x
dsimp
simp only [Set.mem_range, Equiv.ofInjective_symm_apply, dite_eq_right_iff, forall_exists_index]
intro y e
have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩
rw [disjoint_iff.mp h₃.1] at this
exact this.elim
· rintro T _ _ m rfl rfl
funext x
dsimp
split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm
