English
Let X be an object of C and S a sieve on X. There exists an object Y and a morphism π: Y → X which is an effective epimorphism, such that the arrows of π lie in S (i.e. S.arrows π holds). This is equivalent to saying that S belongs to the induced topology F.inducedTopology (regularTopology _) X.
Русский
Пусть X − объект категории C и S — сетка на X. Существуют Y и морфизм π: Y → X, который является эффективной эпиморфией, причём стрелки π лежат в S (S.arrows π). Это эквивалентно тому, что S ∈ F.inducedTopology (regularTopology _) X.
LaTeX
$$$\left(\exists Y\; (\pi:\,Y\to X),\ text{EffectiveEpi }\pi\ \wedge\ S.arrows\pi\right) \iff \left(S \in F.inducedTopology(regularTopology\,\_)\, X\right)$$$
Lean4
theorem exists_effectiveEpi_iff_mem_induced (X : C) (S : Sieve X) :
(∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) ↔ (S ∈ F.inducedTopology (regularTopology _) X) :=
by
refine ⟨fun ⟨Y, π, ⟨H₁, H₂⟩⟩ ↦ ?_, fun hS ↦ ?_⟩
· apply (mem_sieves_iff_hasEffectiveEpi (Sieve.functorPushforward _ S)).mpr
refine ⟨F.obj Y, F.map π, ⟨?_, Sieve.image_mem_functorPushforward F S H₂⟩⟩
exact F.map_effectiveEpi _
· obtain ⟨Y, π, ⟨H₁, H₂⟩⟩ := (mem_sieves_iff_hasEffectiveEpi _).mp hS
let g₀ := F.effectiveEpiOver Y
refine ⟨_, F.preimage (g₀ ≫ π), ?_, (?_ : S.arrows (F.preimage _))⟩
· refine F.effectiveEpi_of_map _ ?_
simp only [map_preimage]
infer_instance
· obtain ⟨W, g₁, g₂, h₁, h₂⟩ := H₂
rw [h₂]
convert S.downward_closed h₁ (F.preimage (g₀ ≫ g₂))
exact F.map_injective (by simp)
