English
Equivalence of induced topologies: the coherent topology equals the induced topology under appropriate assumptions.
Русский
Равенство когерентной топологии с индуцированной топологией при заданных предпосылках.
LaTeX
$$eq_induced$$
Lean4
theorem exists_effectiveEpiFamily_iff_mem_induced (X : C) (S : Sieve X) :
(∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → (Y a ⟶ X)),
EffectiveEpiFamily Y π ∧ (∀ a : α, (S.arrows) (π a))) ↔
(S ∈ F.inducedTopology (coherentTopology _) X) :=
by
refine ⟨fun ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ ↦ ?_, fun hS ↦ ?_⟩
· apply (mem_sieves_iff_hasEffectiveEpiFamily (Sieve.functorPushforward _ S)).mpr
refine
⟨α, inferInstance, fun i => F.obj (Y i), fun i => F.map (π i),
⟨?_, fun a => Sieve.image_mem_functorPushforward F S (H₂ a)⟩⟩
exact F.map_finite_effectiveEpiFamily _ _
· obtain ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ := (mem_sieves_iff_hasEffectiveEpiFamily _).mp hS
refine ⟨α, inferInstance, ?_⟩
let Z : α → C := fun a ↦ (Functor.EffectivelyEnough.presentation (F := F) (Y a)).some.p
let g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun a ↦ F.effectiveEpiOver (Y a)
have : EffectiveEpiFamily _ (fun a ↦ g₀ a ≫ π a) := inferInstance
refine ⟨Z, fun a ↦ F.preimage (g₀ a ≫ π a), ?_, fun a ↦ (?_ : S.arrows (F.preimage _))⟩
· refine F.finite_effectiveEpiFamily_of_map _ _ ?_
simpa using this
· obtain ⟨W, g₁, g₂, h₁, h₂⟩ := H₂ a
rw [h₂]
convert S.downward_closed h₁ (F.preimage (g₀ a ≫ g₂))
exact F.map_injective (by simp)
