thin_diagram_of_surjective — Mathlib

English

For any f : i ⟶ j, eventualRange(j) = range(F.map f) holds if and only if for all k and g : k ⟶ i, range(F.map f) ⊆ range(F.map (g ≫ f)).

Русский

Для любого f : i ⟶ j условие eventualRange(j) = range(F.map f) эквивалентно тому, что для всех k и g : k ⟶ i имеет место inclusion: range(F.map f) ⊆ range(F.map (g ≫ f)).

LaTeX

$$$F.eventualRange(j) = \mathrm{range}(F.map f) \iff \forall k\; \forall g : k \to i, \, \mathrm{range}(F.map f) \subseteq \mathrm{range}(F.map (g \circ f)).$$$

Lean4

/-- If `F` has all arrows surjective, then it "factors through a poset". -/
theorem thin_diagram_of_surjective (Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), (F.map f).Surjective) {i j} (f g : i ⟶ j) :
    F.map f = F.map g :=
  let ⟨k, φ, hφ⟩ := IsCofilteredOrEmpty.cone_maps f g
  (Fsur φ).injective_comp_right <| by simp_rw [← types_comp, ← F.map_comp, hφ]

Похожие утверждения