instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget

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]

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