functor_galoisConnection — Mathlib

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

Похожие утверждения