English
Let J be a small filtered category, R a commutative ring, and F: J ⥤ CommRingCat. For S over R which is essentially of finite type, and two R-algebra morphisms a: S ⟶ F.obj i and b: S ⟶ F.obj j that agree on the colimit, there exists k with morphisms i ⟶ k and j ⟶ k such that a maps to b after passing to F.obj k; i.e., the map colim_i Hom_R(S, F.obj i) → Hom_R(S, colim F) is injective.
Русский
Пусть J — малая фильтрованная категория, R — коммутативное кольцо, F: J ⥤ CommRingCat. Пусть S над R является по существу конечного типа; если две гомоморфизмы a: S ⟶ F.i и b: S ⟶ F.j согласованы при переходе к колимиту, то существуют k и орты i ⟶ k, j ⟶ k такие, что a ∘ F.map hik = b ∘ F.map hjk; т.е. инъективность перехода из колимита гомоморфизмов.
LaTeX
$$$\exists k\ (\hik : i \to k)\ (\hjk : j \to k),\ a \circ F.map \hik = b \circ F.map \hjk$$$
Lean4
/-- Given a filtered diagram `F` of rings over `R`, `S` an (essentially) of finite type `R`-algebra,
and two ring homs `a : S ⟶ Fᵢ` and `b : S ⟶ Fⱼ` over `R`.
If `a` and `b` agree at `S ⟶ colimit F`,
then there exists `k` such that `a` and `b` are equal at `S ⟶ F_k`.
In other words, the map `colimᵢ Hom_R(S, Fᵢ) ⟶ Hom_R(S, colim F)` is injective.
-/
theorem exists_comp_map_eq_of_isColimit (hf : f.hom.EssFiniteType) {i : J} (a : S ⟶ F.obj i) (ha : f ≫ a = α.app i)
{j : J} (b : S ⟶ F.obj j) (hb : f ≫ b = α.app j) (hab : a ≫ c.ι.app i = b ≫ c.ι.app j) :
∃ (k : J) (hik : i ⟶ k) (hjk : j ⟶ k), a ≫ F.map hik = b ≫ F.map hjk := by
classical
have hc' := isColimitOfPreserves (forget _) hc
choose k f₁ f₂ h using fun x : S ↦ (Types.FilteredColimit.isColimit_eq_iff _ hc').mp congr(($hab).hom x)
let J' : MulticospanShape := ⟨Unit ⊕ Unit, hf.finset, fun _ ↦ .inl .unit, fun _ ↦ .inr .unit⟩
let D : MulticospanIndex J' J :=
{ left := Sum.elim (fun _ ↦ i) (fun _ ↦ j)
right x := k x.1
fst x := f₁ x
snd x := f₂ x }
obtain ⟨c'⟩ := IsFiltered.cocone_nonempty D.multicospan
refine ⟨c'.pt, c'.ι.app (.left (.inl .unit)), c'.ι.app (.left (.inr .unit)), ?_⟩
ext1
apply hf.ext
· rw [← CommRingCat.hom_comp, ← CommRingCat.hom_comp, reassoc_of% ha, reassoc_of% hb]
simp [← α.naturality]
· intro x hx
rw [← c'.w (.fst (by exact ⟨x, hx⟩)), ← c'.w (.snd (by exact ⟨x, hx⟩))]
have (x : _) : F.map (f₁ x) (a x) = F.map (f₂ x) (b x) := h x
simp [D, this]
