English
The extensive and regular coverages generate the coherent topology on C (same as above with variant).
Русский
Обширная и регулярная покрытия порождают когерентную топологию на C (вариант формулировки).
LaTeX
$$$\text{coherentTopology}(C) = (\mathrm{extensiveCoverage}(C) \sqcup \mathrm{regularCoverage}(C)).toGrothendieck$$$
Lean4
/-- The union of the extensive and regular coverages generates the coherent topology on `C`. -/
theorem extensive_regular_generate_coherent [Preregular C] [FinitaryPreExtensive C] :
((extensiveCoverage C) ⊔ (regularCoverage C)).toGrothendieck = (coherentTopology C) :=
by
ext B S
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
·
induction h with
| of Y T hT =>
apply Coverage.Saturate.of
simp only [Coverage.sup_covering, Set.mem_union] at hT
exact
Or.elim hT (fun ⟨α, x, X, π, ⟨h, _⟩⟩ ↦ ⟨α, x, X, π, ⟨h, inferInstance⟩⟩)
(fun ⟨Z, f, ⟨h, _⟩⟩ ↦ ⟨Unit, inferInstance, fun _ ↦ Z, fun _ ↦ f, ⟨h, inferInstance⟩⟩)
| top => apply Coverage.Saturate.top
| transitive Y T => apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]
·
induction h with
| of Y T hT =>
obtain ⟨I, _, X, f, rfl, hT⟩ := hT
apply
Coverage.Saturate.transitive Y
(generate (Presieve.ofArrows (fun (_ : Unit) ↦ (∐ fun (i : I) => X i)) (fun (_ : Unit) ↦ Sigma.desc f)))
· apply Coverage.Saturate.of
simp only [Coverage.sup_covering, extensiveCoverage, regularCoverage, Set.mem_union, Set.mem_setOf_eq]
exact Or.inr ⟨_, Sigma.desc f, ⟨rfl, inferInstance⟩⟩
· rintro R g ⟨W, ψ, σ, ⟨⟩, rfl⟩
change _ ∈ ((extensiveCoverage C) ⊔ (regularCoverage C)).toGrothendieck R
rw [Sieve.pullback_comp]
apply pullback_stable
have :
generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i) ≤
(generate (Presieve.ofArrows X f)).pullback (Sigma.desc f) :=
by
rintro Q q ⟨E, e, r, ⟨hq, rfl⟩⟩
exact ⟨E, e, r ≫ (Sigma.desc f), by cases hq; simpa using Presieve.ofArrows.mk _, by simp⟩
apply Coverage.saturate_of_superset _ this
apply Coverage.Saturate.of
refine Or.inl ⟨I, inferInstance, _, _, ⟨rfl, ?_⟩⟩
convert IsIso.id _
aesop
| top => apply Coverage.Saturate.top
| transitive Y T => apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]
