English
If C is filtered-or-empty and for every d there exists c with a morphism d → F.obj c, and a certain compatibility holds, then StructuredArrow d F is filtered for every d.
Русский
Если C фильтрована или пуста и для каждого d существует c с морфизмом d → F.obj c, и выполняется совместимость, то StructuredArrow d F фильтрована для каждого d.
LaTeX
$$$\\mathrm{IsFilteredOrEmpty}(C) \\land \\bigl( \\forall d, \\exists c, \\mathrm{Nonempty}(d \\to F.obj c) \\bigr) \\land \\bigl( \\forall {d,c}(s,s' : d \\to F.obj c), \\exists c', t, s \\;\\text{и} \\; F.map t = s'\\;\\text{совпадает} \\bigr) \\Rightarrow \\forall d, \\mathrm{IsFiltered}(\\mathrm{StructuredArrow}\\, d\\, F)$$$
Lean4
theorem isFiltered_structuredArrow_of_isFiltered_of_exists [IsFilteredOrEmpty C] (h₁ : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c))
(h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) (d : D) :
IsFiltered (StructuredArrow d F) :=
by
have : Nonempty (StructuredArrow d F) := by
obtain ⟨c, ⟨f⟩⟩ := h₁ d
exact ⟨.mk f⟩
suffices IsFilteredOrEmpty (StructuredArrow d F) from IsFiltered.mk
refine ⟨fun f g => ?_, fun f g η μ => ?_⟩
· obtain ⟨c, ⟨t, ht⟩⟩ :=
h₂ (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right))
refine ⟨.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t)), ?_, ?_, trivial⟩
· exact StructuredArrow.homMk (IsFiltered.leftToMax _ _ ≫ t) rfl
· exact StructuredArrow.homMk (IsFiltered.rightToMax _ _ ≫ t) (by simpa using ht.symm)
· refine
⟨.mk (f.hom ≫ F.map (η.right ≫ IsFiltered.coeqHom η.right μ.right)),
StructuredArrow.homMk (IsFiltered.coeqHom η.right μ.right) (by simp), ?_⟩
simpa using IsFiltered.coeq_condition _ _
