English
If C is a Grothendieck abelian category and F: J ⥤ MonoOver X is a functor from a κ-filtered category, then there exists an index j ∈ J such that (F.obj j).obj.hom is an isomorphism.
Русский
Если C — абелева категория Гротендикта и F: J ⥤ MonoOver X — функтор из κ-фильтрованной категории, то существует координата j ∈ J, такая что (F.obj j).obj.hom является изоморфизмом.
LaTeX
$$$\exists j:\, J,\; IsIso\bigl((F.obj j).obj.hom\bigr)$$$
Lean4
/-- If `C` is a Grothendieck abelian category, `X : C`, if `F : J ⥤ MonoOver X` is a
functor from a `κ`-filtered category `J` with `κ` a regular cardinal such
that `HasCardinalLT (Subobject X) κ`, and if the colimit of `F` (computed in `C`)
maps epimorphically onto `X`, then there exists `j : J` such that `(F.obj j).obj.hom`
is an isomorphism. -/
theorem exists_isIso_of_functor_from_monoOver {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ]
(hXκ : HasCardinalLT (Subobject X) κ) (c : Cocone (F ⋙ MonoOver.forget _ ⋙ Over.forget _)) (hc : IsColimit c)
(f : c.pt ⟶ X) (hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom) (h : Epi f) :
∃ (j : J), IsIso (F.obj j).obj.hom :=
by
have := isFiltered_of_isCardinalFiltered J κ
have := mono_of_isColimit_monoOver F hc f hf
rw [Subobject.epi_iff_mk_eq_top f, subobjectMk_of_isColimit_eq_iSup F hc f hf] at h
let s (j : J) : Subobject X := Subobject.mk (F.obj j).obj.hom
have h' : Function.Surjective (fun (j : J) ↦ (⟨s j, _, rfl⟩ : Set.range s)) :=
by
rintro ⟨_, j, rfl⟩
exact ⟨j, rfl⟩
obtain ⟨σ, hσ⟩ := h'.hasRightInverse
have hs : HasCardinalLT (Set.range s) κ := hXκ.of_injective (f := Subtype.val) Subtype.val_injective
refine ⟨IsCardinalFiltered.max σ hs, ?_⟩
rw [Subobject.isIso_iff_mk_eq_top, ← top_le_iff, ← h, iSup_le_iff]
intro j
let t : Set.range s := ⟨_, j, rfl⟩
trans Subobject.mk (F.obj (σ t)).obj.hom
· exact (hσ t).symm.le
· exact MonoOver.subobjectMk_le_mk_of_hom (F.map (IsCardinalFiltered.toMax σ hs t))
