Lean4
/-- The trivial pretopology, in which the coverings are exactly singleton isomorphisms. This topology is
also known as the indiscrete, coarse, or chaotic topology. -/
@[stacks 07GE]
def trivial : Pretopology C
where
coverings X S := ∃ (Y : _) (f : Y ⟶ X) (_ : IsIso f), S = Presieve.singleton f
has_isos _ _ _ i := ⟨_, _, i, rfl⟩
pullbacks X Y f
S := by
rintro ⟨Z, g, i, rfl⟩
refine ⟨pullback g f, pullback.snd _ _, ?_, ?_⟩
· refine ⟨⟨pullback.lift (f ≫ inv g) (𝟙 _) (by simp), ⟨?_, by simp⟩⟩⟩
ext
· rw [assoc, pullback.lift_fst, ← pullback.condition_assoc]
simp
· simp
· apply pullback_singleton
transitive := by
rintro X S Ti ⟨Z, g, i, rfl⟩ hS
rcases hS g (singleton_self g) with ⟨Y, f, i, hTi⟩
refine ⟨_, f ≫ g, ?_, ?_⟩
·
infer_instance
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): the next four lines were just "ext (W k)"
apply funext
rintro W
apply Set.ext
rintro k
constructor
· rintro ⟨V, h, k, ⟨_⟩, hh, rfl⟩
rw [hTi] at hh
cases hh
apply singleton.mk
· rintro ⟨_⟩
refine bind_comp g singleton.mk ?_
rw [hTi]
apply singleton.mk
