Lean4
/-- If a functor `G : C ⥤ (D, K)` is fully faithful and locally dense,
then the set `{ T ∩ mor(C) | T ∈ K }` is a Grothendieck topology of `C`.
-/
@[simps]
def inducedTopology : GrothendieckTopology C
where
sieves _ S := K _ (S.functorPushforward G)
top_mem'
X := by
change K _ _
rw [Sieve.functorPushforward_top]
exact K.top_mem _
pullback_stable' X Y S iYX
hS :=
by
apply K.transitive (LocallyCoverDense.functorPushforward_functorPullback_mem ⟨_, K.pullback_stable (G.map iYX) hS⟩)
rintro Z _ ⟨U, iUY, iZU, ⟨W, iWX, iUW, hiWX, e₁⟩, rfl⟩
rw [Sieve.pullback_comp]
apply K.pullback_stable
clear iZU Z
apply K.transitive (G.functorPushforward_imageSieve_mem _ iUW)
rintro Z _ ⟨U₁, iU₁U, iZU₁, ⟨iU₁W, e₂⟩, rfl⟩
rw [Sieve.pullback_comp]
apply K.pullback_stable
clear iZU₁ Z
apply
K.superset_covering ?_ (G.functorPushforward_equalizer_mem _ (iU₁U ≫ iUY ≫ iYX) (iU₁W ≫ iWX) (by simp [e₁, e₂]))
rintro Z _ ⟨U₂, iU₂U₁, iZU₂, e₃ : _ = _, rfl⟩
refine ⟨_, iU₂U₁ ≫ iU₁U ≫ iUY, iZU₂, ?_, by simp⟩
simpa [e₃] using S.downward_closed hiWX (iU₂U₁ ≫ iU₁W)
transitive' X S hS S'
H' := by
apply K.transitive hS
rintro Y _ ⟨Z, g, i, hg, rfl⟩
rw [Sieve.pullback_comp]
apply K.pullback_stable i
refine K.superset_covering ?_ (H' hg)
rintro W _ ⟨Z', g', i', hg, rfl⟩
refine ⟨Z', g' ≫ g, i', hg, ?_⟩
simp
