topology_eq_iff_same_sheaves — Mathlib

English

If being a sheaf for J1 is equivalent to being a sheaf for J2, then J1 = J2.

Русский

Если тождественно выполняется в терминах шейфов, что быть шейфом по J1 эквивалентно быть шейфом по J2, то J1 = J2.

LaTeX

$$$J_1 = J_2 \iff \forall P, \big(\mathrm{Presieve.IsSheaf}(J_1, P) \iff \mathrm{Presieve.IsSheaf}(J_2, P)\big)$$$

Lean4

/-- If being a sheaf for `J₁` is equivalent to being a sheaf for `J₂`, then `J₁ = J₂`. -/
theorem topology_eq_iff_same_sheaves {J₁ J₂ : GrothendieckTopology C} :
    J₁ = J₂ ↔ ∀ P : Cᵒᵖ ⥤ Type max v u, Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P :=
  by
  constructor
  · rintro rfl
    intro P
    rfl
  · intro h
    apply le_antisymm
    · apply le_topology_of_closedSieves_isSheaf
      rw [h]
      apply classifier_isSheaf
    · apply le_topology_of_closedSieves_isSheaf
      rw [← h]
      apply classifier_isSheaf

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