English
Under the same hypotheses as the surjectivity lemma, if the images of two elements x1, x2 in the apex under the map from X.obj j coincide after applying the appropriate X.map with a connecting morphism, then there exists a j' and a morphism j→j' witnessing their equality after reindexing along j→j'.
Русский
При тех же предположениях, что и в лемме сюръективности, если образы элементов x1, x2 совпадают после применения соответствующего отображения X.map с некоторым отображением, существует j' и морфизм j→j', доказывающий равенство после ребинирования.
LaTeX
$$$\exists j'\,\alpha:\! j\to j',\ c.pt.map(X.map\alpha)\,x_1 = c.pt.map(X.map\alpha)\,x_2$$$
Lean4
theorem injective (j : J) (x₁ x₂ : c.pt.obj (X.obj j)) (h : c.pt.map (cX.ι.app j) x₁ = c.pt.map (cX.ι.app j) x₂) :
∃ (j' : J) (α : j ⟶ j'), c.pt.map (X.map α) x₁ = c.pt.map (X.map α) x₂ :=
by
have := isFiltered_of_isCardinalFiltered J κ
let y₁ := Types.isLimitEquivSections (hc (X.obj j)) x₁
let y₂ := Types.isLimitEquivSections (hc (X.obj j)) x₂
have hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁ := by simp [y₁]
have hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂ := by simp [y₂]
have H (k : K) :=
(Types.FilteredColimit.isColimit_eq_iff' (ht := hF k) (x := y₁.1 k) (y := y₂.1 k)).1
(by
simp only [y₁, y₂, Types.isLimitEquivSections_apply]
dsimp
simp only [← FunctorToTypes.naturality, h])
let j₁ (k : K) : J := (H k).choose
let f (k : K) : j ⟶ j₁ k := (H k).choose_spec.choose
have hf (k : K) : (F.obj k).map (X.map (f k)) (y₁.1 k) = (F.obj k).map (X.map (f k)) (y₂.1 k) :=
(H k).choose_spec.choose_spec
have hK' := hasCardinalLT_of_hasCardinalLT_arrow hK
let ψ (k : K) : j ⟶ IsCardinalFiltered.max j₁ hK' := f k ≫ IsCardinalFiltered.toMax j₁ hK' k
refine ⟨IsCardinalFiltered.coeq ψ hK', IsCardinalFiltered.toCoeq ψ hK', ?_⟩
apply (Types.isLimitEquivSections (hc _)).injective
ext k
simp only [Types.isLimitEquivSections_apply, ← hy₁, ← hy₂]
have h₁ := Types.isLimitEquivSections_symm_apply (hc (X.obj j)) y₁ k
have h₂ := Types.isLimitEquivSections_symm_apply (hc (X.obj j)) y₂ k
dsimp at h₁ h₂ ⊢
simp only [FunctorToTypes.naturality, h₁, h₂, ← IsCardinalFiltered.coeq_condition ψ hK' k, map_comp,
FunctorToTypes.map_comp_apply, ψ, hf]
