gi — Mathlib · SciLib

Lean4
/-- The two constructions `Coverage.toGrothendieck` and `Coverage.ofGrothendieck` form
a Galois insertion.
-/
def gi : GaloisInsertion (toGrothendieck (C := C)) (GrothendieckTopology.toCoverage (C := C))
    where
  choice K _ := toGrothendieck K
  choice_eq := fun _ _ => rfl
  le_l_u J X S
    hS := by
    rw [← Sieve.generate_sieve S]
    apply Saturate.of
    dsimp [GrothendieckTopology.toCoverage]
    rwa [Sieve.generate_sieve S]
  gc K
    J := by
    constructor
    · intro H X S hS
      exact H _ <| Saturate.of _ _ hS
    · intro H X S hS
      induction hS with
      | of X S hS => exact H _ hS
      | top => apply J.top_mem
      | transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
Похожие утверждения