English
The pair (pushforward F, pullback F) forms a Galois connection between sieves on X and sieves on F.obj X.
Русский
Пара (pushforward F, pullback F) образует галоисовую связь между ситами на X и ситами на F.obj X.
LaTeX
$$$ \\text{GaloisConnection} (Sieve.functorPushforward F) (Sieve.functorPullback F) $$$
Lean4
theorem functor_galoisConnection (X : C) :
GaloisConnection (Sieve.functorPushforward F : Sieve X → Sieve (F.obj X)) (Sieve.functorPullback F) :=
by
intro R S
constructor
· intro hle X f hf
apply hle
refine ⟨X, f, 𝟙 _, hf, ?_⟩
rw [id_comp]
· rintro hle Y f ⟨X, g, h, hg, rfl⟩
apply Sieve.downward_closed S
exact hle g hg