English
There is an instance that asserts that the forgetful functor composed with the locall y directed cover is locally directed.
Русский
Существуют инстансы, задающие локальную направляемость композиции функторов с покрытием.
LaTeX
$$$(\mathcal{U}.functorOfLocallyDirected \circ forget).IsLocallyDirected$$$
Lean4
instance : (𝒰.functorOfLocallyDirected ⋙ Scheme.forget).IsLocallyDirected where
cond {i j k} fi fj xi xj
hxij :=
by
simp only [Functor.comp_obj, Cover.functorOfLocallyDirected_obj, forget_obj, Functor.comp_map,
Cover.functorOfLocallyDirected_map, forget_map] at hxij
have : (𝒰.f i).base xi = (𝒰.f j).base xj := by
rw [← 𝒰.trans_map fi, ← 𝒰.trans_map fj, comp_base, comp_base, ConcreteCategory.comp_apply, hxij,
ConcreteCategory.comp_apply]
obtain ⟨z, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback xi xj this
obtain ⟨l, gi, gj, y, rfl⟩ := 𝒰.exists_lift_trans_eq z
refine ⟨l, gi, gj, y, ?_, ?_⟩ <;> simp [← Scheme.comp_base_apply]