English
A sieve is in the coherent topology iff it contains a finite EffectiveEpiFamily of arrows.
Русский
Сита наложено когерентной топологией тогда и только тогда, когда содержит конечную EffectiveEpiFamily стрелок.
LaTeX
$$$(S \in \mathrm{coherentTopology}\ C X) \iff \exists α\ (Finite α)\ (Y: α \to C) (π: (a:α) \to (Y a \to X)),\; EffectiveEpiFamily Y π \wedge \forall a, S.arrows(π a)$$$
Lean4
/-- A sieve belongs to the coherent topology if and only if it contains a finite
`EffectiveEpiFamily`.
-/
theorem mem_sieves_iff_hasEffectiveEpiFamily (S : Sieve X) :
(S ∈ (coherentTopology C) X) ↔
(∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → (Y a ⟶ X)),
EffectiveEpiFamily Y π ∧ (∀ a : α, (S.arrows) (π a))) :=
by
constructor
· intro h
induction h with
| of Y T hS =>
obtain ⟨a, h, Y', π, h', _⟩ := hS
refine ⟨a, h, Y', π, inferInstance, fun a' ↦ ?_⟩
obtain ⟨rfl, _⟩ := h'
exact ⟨Y' a', 𝟙 Y' a', π a', Presieve.ofArrows.mk a', by simp⟩
| top Y => exact ⟨Unit, inferInstance, fun _ => Y, fun _ => (𝟙 Y), inferInstance, by simp⟩
| transitive Y R S _ _ a b =>
obtain ⟨α, w, Y₁, π, ⟨h₁, h₂⟩⟩ := a
choose β _ Y_n π_n H using fun a => b (h₂ a)
exact
⟨(Σ a, β a), inferInstance, fun ⟨a, b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1), fun c => (H c.fst).2 c.snd⟩
· exact coherentTopology.mem_sieves_of_hasEffectiveEpiFamily S
