instIsLocallyDirectedWidePushoutShapeOfMonoObjNoneSomeMapInit

English

For a functor into Type indexed by a wide pushout shape, if each map from the initial objects is mono, the diagram is locally directed; in particular, one can lift arrows into the pushout in a directed way.

Русский

Для функторa в Type, индексированного широким пуш-оутShape, если отображения из начальных объектов монофункциональные, диаграмма локально направлена; в частности, можно подобрать подъемы стрелок в пуш-аут последовательно.

LaTeX

$$$$\\text{LocallyDirected}(F) \\quad\\text{for }F: \\text{WidePushoutShape } J \\to \\mathbf{Type} \\text{ with Mono on init maps}$$$$

Lean4

instance (F : WidePushoutShape J ⥤ Type*) [∀ i, Mono (F.map (.init i))] : F.IsLocallyDirected :=
  by
  constructor
  rintro i j k (_ | i) (_ | j)
  · simp only [WidePushoutShape.hom_id, FunctorToTypes.map_id_apply, forall_eq']
    exact fun x ↦ ⟨_, 𝟙 _, 𝟙 _, x, by simp⟩
  · simp only [WidePushoutShape.hom_id, FunctorToTypes.map_id_apply, forall_comm, forall_eq]
    exact fun x ↦ ⟨_, .init _, 𝟙 _, x, by simp⟩
  · simp only [WidePushoutShape.hom_id, FunctorToTypes.map_id_apply, forall_eq']
    exact fun x ↦ ⟨_, 𝟙 _, .init _, x, by simp⟩
  · simp only [((CategoryTheory.mono_iff_injective (F.map (.init i))).mp inferInstance).eq_iff, forall_eq']
    exact fun x ↦ ⟨_, 𝟙 _, 𝟙 _, x, by simp⟩

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