English
The class of monomorphisms in Type u is stable under filtered colimits.
Русский
Класс мономорфизмов в Type u устойчив к филтрованным колимитам.
LaTeX
$$$ (\\text{monomorphisms }(\\mathrm{Type}\\, u)).IsStableUnderFilteredColimits $$$
Lean4
instance : MorphismProperty.IsStableUnderFilteredColimits.{v', u'} (monomorphisms (Type u)) where
isStableUnderColimitsOfShape J _
_ :=
⟨fun F₁ F₂ c₁ c₂ hc₁ hc₂ f hf φ hφ ↦
by
simp only [functorCategory, monomorphisms.iff, mono_iff_injective] at hf ⊢
replace hφ (j : J) := congr_fun (hφ j)
dsimp at hφ
intro x₁ y₁ h
obtain ⟨j, x₁, y₁, rfl, rfl⟩ : ∃ (j : J) (x₁' y₁' : F₁.obj j), x₁ = c₁.ι.app j x₁' ∧ y₁ = c₁.ι.app j y₁' :=
by
obtain ⟨j, x₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ x₁
obtain ⟨l, y₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ y₁
exact
⟨_, _, _, congr_fun (c₁.w (IsFiltered.leftToMax j l)).symm _,
congr_fun (c₁.w (IsFiltered.rightToMax j l)).symm _⟩
rw [hφ, hφ] at h
obtain ⟨k, α, hk⟩ := (Types.FilteredColimit.isColimit_eq_iff' hc₂ _ _).1 h
simp only [← FunctorToTypes.naturality] at hk
rw [← c₁.w α, types_comp_apply, types_comp_apply, hf _ hk]⟩
