English
Let x be a point in the apex of a cocone c over a diagram F with suitable hypotheses; then x arises as the image of some element from one of the components X.obj j under the cocone maps. More precisely, x = (c.pt.mapCocone cX).ι.app j x' for some j and x'.
Русский
Пусть x — элемент вершины кокона c над диаграммой F при допустимых предположениях; тогда x является образом некоторого элемента из компоненты X.obj j под коконным отображением. То есть существует j и x' с x = (c.pt.mapCocone cX).ι.app j x'.
LaTeX
$$$\forall x\in c.pt,\ \exists j\in J,\ x'\in (c.pt.obj(X.obj\,j)),\ x=(c.pt.mapCocone\ cX).ι.app\ j\ x'$$$
Lean4
theorem surjective (x : c.pt.obj cX.pt) : ∃ (j : J) (x' : c.pt.obj (X.obj j)), x = (c.pt.mapCocone cX).ι.app j x' :=
by
have := isFiltered_of_isCardinalFiltered J κ
obtain ⟨y, hy⟩ := (Types.isLimitEquivSections (hc cX.pt)).symm.surjective x
obtain ⟨j₀, z, hz⟩ :
∃ (j₀ : J) (z : (k : K) → (F.obj k).obj (X.obj j₀)), ∀ (k : K), y.1 k = (F.obj k).map (cX.ι.app j₀) (z k) :=
by
have H (k : K) := Types.jointly_surjective_of_isColimit (hF k) (y.1 k)
let j (k : K) : J := (H k).choose
let z (k : K) : (F.obj k).obj (X.obj (j k)) := (H k).choose_spec.choose
have hz (k : K) : (F.obj k).map (cX.ι.app (j k)) (z k) = y.1 k := (H k).choose_spec.choose_spec
exact
⟨IsCardinalFiltered.max j (hasCardinalLT_of_hasCardinalLT_arrow hK), fun k ↦
(F.obj k).map (X.map (IsCardinalFiltered.toMax j _ k)) (z k), fun k ↦ by
rw [← hz, ← FunctorToTypes.map_comp_apply, cX.w]⟩
obtain ⟨j₁, α, hα⟩ :
∃ (j₁ : J) (α : j₀ ⟶ j₁),
∀ ⦃k k' : K⦄ (φ : k ⟶ k'), (F.obj k').map (X.map α) ((F.map φ).app _ (z k)) = (F.obj k').map (X.map α) (z k') :=
by
have H {k k' : K} (φ : k ⟶ k') :=
(Types.FilteredColimit.isColimit_eq_iff' (ht := hF k') (x := (F.map φ).app _ (z k)) (y := z k')).1
(by
dsimp
simpa only [← FunctorToTypes.naturality, ← hz] using y.2 φ)
let j {k k' : K} (φ : k ⟶ k') : J := (H φ).choose
let g {k k' : K} (φ : k ⟶ k') : j₀ ⟶ j φ := (H φ).choose_spec.choose
have hg {k k' : K} (φ : k ⟶ k') :
(F.obj k').map (X.map (g φ)) ((F.map φ).app _ (z k)) = (F.obj k').map (X.map (g φ)) (z k') :=
(H φ).choose_spec.choose_spec
obtain ⟨j₁, α, β, hα⟩ :
∃ (j₁ : J) (α : j₀ ⟶ j₁) (β : ∀ ⦃k k' : K⦄ (φ : k ⟶ k'), j φ ⟶ j₁), ∀ ⦃k k' : K⦄ (φ : k ⟶ k'), α = g φ ≫ β φ :=
by
let j'' (f : Arrow K) : J := j f.hom
let ψ (f : Arrow K) : j₀ ⟶ IsCardinalFiltered.max j'' hK := g f.hom ≫ IsCardinalFiltered.toMax j'' hK f
refine
⟨IsCardinalFiltered.coeq ψ hK, IsCardinalFiltered.toCoeq ψ hK, fun k k' φ ↦
IsCardinalFiltered.toMax j'' hK φ ≫ IsCardinalFiltered.coeqHom ψ hK, fun k k' φ ↦ ?_⟩
simpa [ψ] using (IsCardinalFiltered.coeq_condition ψ hK (Arrow.mk φ)).symm
exact ⟨j₁, α, fun k k' φ ↦ by simp [hα φ, hg]⟩
let s : (F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).sections :=
{ val k := (F.obj k).map (X.map α) (z k)
property {k k'}
φ := by
dsimp
rw [FunctorToTypes.naturality, ← hα φ] }
refine ⟨j₁, (Types.isLimitEquivSections (hc (X.obj j₁))).symm s, ?_⟩
apply (Types.isLimitEquivSections (hc cX.pt)).injective
rw [← hy, Equiv.apply_symm_apply]
ext k
have h₁ :=
Types.isLimitEquivSections_apply (hc cX.pt) k
(c.pt.map (cX.ι.app j₁) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s))
have h₂ := Types.isLimitEquivSections_symm_apply (hc (X.obj j₁)) s k
dsimp at h₁ h₂ ⊢
rw [h₁, hz, FunctorToTypes.naturality, h₂, ← FunctorToTypes.map_comp_apply, cX.w]
