English
A binary cofan is a colimit if and only if the legs are open embeddings and the images of the two legs form a disjoint covering of their union, i.e., they are complementary.
Русский
Двойной кофан является колимитом тогда и только тогда, когда его ножки являются открытыми вложениями, их образы образуют раздельное покрытие их объединения и т. п.
LaTeX
$$$\\text{Nonempty}(\\mathrm{IsColimit}\,c) \\iff \\text{IsOpenEmbedding}\,c.inl \\land \\text{IsOpenEmbedding}\,c.inr \\land \\text{IsCompl}(\\operatorname{range} c.inl)(\\operatorname{range} c.inr)$$$
Lean4
theorem binaryCofan_isColimit_iff {X Y : TopCat} (c : BinaryCofan X Y) :
Nonempty (IsColimit c) ↔ IsOpenEmbedding c.inl ∧ IsOpenEmbedding c.inr ∧ IsCompl (range c.inl) (range c.inr) := by
classical
constructor
· rintro ⟨h⟩
rw [← show _ = c.inl from h.comp_coconePointUniqueUpToIso_inv (binaryCofanIsColimit X Y) ⟨WalkingPair.left⟩, ←
show _ = c.inr from h.comp_coconePointUniqueUpToIso_inv (binaryCofanIsColimit X Y) ⟨WalkingPair.right⟩]
dsimp
refine
⟨(homeoOfIso <| h.coconePointUniqueUpToIso (binaryCofanIsColimit X Y)).symm.isOpenEmbedding.comp .inl,
(homeoOfIso <| h.coconePointUniqueUpToIso (binaryCofanIsColimit X Y)).symm.isOpenEmbedding.comp .inr, ?_⟩
rw [Set.range_comp, ← eq_compl_iff_isCompl]
conv_rhs => rw [Set.range_comp]
erw [← Set.image_compl_eq (homeoOfIso <| h.coconePointUniqueUpToIso (binaryCofanIsColimit X Y)).symm.bijective,
Set.compl_range_inr, Set.image_comp]
· 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
refine ofHom (ContinuousMap.mk ?_ ?_)
·
exact fun x =>
if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective _ h₁.injective).symm ⟨x, h⟩)
else g ((Equiv.ofInjective _ h₂.injective).symm ⟨x, (this x).resolve_left h⟩)
rw [continuous_iff_continuousAt]
intro x
by_cases h : x ∈ Set.range c.inl
· revert h x
apply (IsOpen.continuousOn_iff _).mp
· rw [continuousOn_iff_continuous_restrict]
convert_to Continuous (f ∘ h₁.isEmbedding.toHomeomorph.symm)
· ext ⟨x, hx⟩
exact dif_pos hx
continuity
· exact h₁.isOpen_range
· revert h x
apply (IsOpen.continuousOn_iff _).mp
· rw [continuousOn_iff_continuous_restrict]
have : ∀ a, a ∉ Set.range c.inl → a ∈ Set.range c.inr :=
by
rintro a (h : a ∈ (Set.range c.inl)ᶜ)
rwa [eq_compl_iff_isCompl.mpr h₃.symm]
convert_to Continuous (g ∘ h₂.isEmbedding.toHomeomorph.symm ∘ Subtype.map _ this)
· ext ⟨x, hx⟩
exact dif_neg hx
apply Continuous.comp
· exact g.hom.continuous_toFun
· apply Continuous.comp
· continuity
· rw [IsEmbedding.subtypeVal.isInducing.continuous_iff]
exact continuous_subtype_val
· change IsOpen (Set.range c.inl)ᶜ
rw [← eq_compl_iff_isCompl.mpr h₃.symm]
exact h₂.isOpen_range
· intro T f g
ext x
dsimp
rw [dif_pos ⟨x, rfl⟩]
conv_lhs => rw [Equiv.ofInjective_symm_apply]
· intro T f g
ext x
dsimp
rw [dif_neg]
· exact congr_arg g (Equiv.ofInjective_symm_apply _ _)
· rintro ⟨y, e⟩
have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩
rwa [disjoint_iff.mp h₃.1] at this
· rintro T _ _ m rfl rfl
ext x
change m x = dite _ _ _
split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm
