English
If C is IsCofilteredOrEmpty and for every d there exists c with Nonempty F.obj c ⟶ d, and a compatibility condition for arrows, then CostructuredArrow F d is cofILTERED.
Русский
Если C кофильтрована или пуста и для каждого d существует c с непустым F.obj c ⟶ d и есть совместимость стрелок, то CostructuredArrow F d кофильтрована.
LaTeX
$$$\\mathrm{IsCofilteredOrEmpty}(C) \\land \\bigl( \\forall d, \\exists c, \\mathrm{Nonempty}(\\mathrm{F.obj}\\, c \\to d) \\bigr) \land \\bigl( \\forall {d,c}(s,s' : \\mathrm{F.obj}\, c \\to d), \\exists c', t, \\mathrm{F.map}\\, t \\;\\text{равно} \\; s \\to d \\bigr) \\Rightarrow \\mathrm{IsCofiltered}(\\mathrm{CostructuredArrow}\\, F\\, d)$$$
Lean4
theorem isCofiltered_costructuredArrow_of_isCofiltered_of_exists [IsCofilteredOrEmpty C]
(h₁ : ∀ d, ∃ c, Nonempty (F.obj c ⟶ d))
(h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') (d : D) :
IsCofiltered (CostructuredArrow F d) :=
by
suffices IsFiltered (CostructuredArrow F d)ᵒᵖ from isCofiltered_of_isFiltered_op _
suffices IsFiltered (StructuredArrow (op d) F.op) from
IsFiltered.of_equivalence (costructuredArrowOpEquivalence _ _).symm
apply isFiltered_structuredArrow_of_isFiltered_of_exists
· intro d
obtain ⟨c, ⟨t⟩⟩ := h₁ d.unop
exact ⟨op c, ⟨Quiver.Hom.op t⟩⟩
· intro d c s s'
obtain ⟨c', t, ht⟩ := h₂ s.unop s'.unop
exact ⟨op c', Quiver.Hom.op t, Quiver.Hom.unop_inj ht⟩
