English
Effective epi families are transitive: composing an EffectiveEpiFamily over a family Y with another over each Y_a yields an EffectiveEpiFamily over the total sum.
Русский
Эффективные эпиморфные семейства транзитивны: композиция семейства EEP над Y и семейства над каждым Y_a образуют новое EEP над суммой.
LaTeX
$$Theorem: transitive_of_finite for EffectiveEpiFamily$$
Lean4
/-- Effective epi families in a precoherent category are transitive, in the sense that an
`EffectiveEpiFamily` and an `EffectiveEpiFamily` over each member, the composition is an
`EffectiveEpiFamily`.
Note: The finiteness condition is an artifact of the proof and is probably unnecessary.
-/
theorem transitive_of_finite {α : Type} [Finite α] {Y : α → C} (π : (a : α) → (Y a ⟶ X)) (h : EffectiveEpiFamily Y π)
{β : α → Type} [∀ (a : α), Finite (β a)] {Y_n : (a : α) → β a → C} (π_n : (a : α) → (b : β a) → (Y_n a b ⟶ Y a))
(H : ∀ a, EffectiveEpiFamily (Y_n a) (π_n a)) :
EffectiveEpiFamily (fun (c : Σ a, β a) => Y_n c.fst c.snd) (fun c => π_n c.fst c.snd ≫ π c.fst) :=
by
rw [← Sieve.effectiveEpimorphic_family]
suffices h₂ :
(Sieve.generate (Presieve.ofArrows (fun (⟨a, b⟩ : Σ _, β _) => Y_n a b) (fun ⟨a, b⟩ => π_n a b ≫ π a))) ∈
(coherentTopology C) X
by
change Nonempty _
rw [← Sieve.forallYonedaIsSheaf_iff_colimit]
exact fun W => coherentTopology.isSheaf_yoneda_obj W _ h₂
apply Coverage.Saturate.transitive X (Sieve.generate (Presieve.ofArrows Y π))
· apply Coverage.Saturate.of
use α, inferInstance, Y, π
· intro V f ⟨Y₁, h, g, ⟨hY, hf⟩⟩
rw [← hf, Sieve.pullback_comp]
apply (coherentTopology C).pullback_stable'
apply coherentTopology.mem_sieves_of_hasEffectiveEpiFamily
obtain ⟨i⟩ := hY
exact
⟨β i, inferInstance, Y_n i, π_n i, H i, fun b ↦
⟨Y_n i b, (𝟙 _), π_n i b ≫ π i, ⟨(⟨i, b⟩ : Σ (i : α), β i)⟩, by simp⟩⟩
