English
Refining the previous injectivity criterion to the case where both elements x and x' lie in the same type F(j). The map F.descColimitType c is injective if and only if for every j ∈ J and x, x' ∈ F(j), equal images c.ι j x = c.ι j x' imply there exists k ∈ J and f: j → k with F.map f x = F.map f x'.
Русский
Уточнение предыдущего критерия инъективности: если элементы x и x' принадлежат одной секции F(j), то инъективность F.descColimitType c эквивалентна тому, что для всех j и x, x' ∈ F(j) из равенства c.ι j x = c.ι j x' следует существование k ∈ J и f: j → k, такого что F.map f x = F.map f x'.
LaTeX
$$$$ \text{Injective}(F.descColimitType\, c) \iff \forall j:\, J, \forall x,x':\, F(j),\ c.\iota j x = c.\iota j x' \to \exists k:\, J, \exists f: j \to k, F.map f x = F.map f x'. $$$$
Lean4
/-- Variant of `descColimitType_injective_iff_of_isFiltered` where we
assume both elements `x` and `x'` are in the same type `F.obj j`. -/
theorem descColimitType_injective_iff_of_isFiltered' :
Function.Injective (F.descColimitType c) ↔
∀ (j : J) (x x' : F.obj j), c.ι j x = c.ι j x' → ∃ (k : J) (f : j ⟶ k), F.map f x = F.map f x' :=
by
rw [descColimitType_injective_iff_of_isFiltered]
constructor
· intro h j x x' eq
obtain ⟨k, f, f', eq⟩ := h _ _ _ _ eq
refine ⟨coeq f f', f ≫ coeqHom f f', ?_⟩
rw [FunctorToTypes.map_comp_apply, eq, ← FunctorToTypes.map_comp_apply, coeq_condition]
· intro h j j' x x' eq
obtain ⟨k, g, eq⟩ :=
h (max j j') (F.map (leftToMax _ _) x) (F.map (rightToMax _ _) x') (by simpa only [c.ι_naturality_apply])
exact ⟨k, leftToMax _ _ ≫ g, rightToMax _ _ ≫ g, by simp only [FunctorToTypes.map_comp_apply, eq]⟩
