overGrothendieckTopology_eq_toGrothendieck_overPretopology

English

Reduction showing that over Grothendieck topology equals to the Grothendieck topology induced by the pretopology via forgetful functors.

Русский

Преобразование показывает, что надмножество равняется, через запоминание, топологии Гротендика.

LaTeX

$$$S.overGrothendieckTopology P = (S.overPretopology P).toGrothendieck$$$

Lean4

theorem overGrothendieckTopology_eq_toGrothendieck_overPretopology :
    S.overGrothendieckTopology P = (S.overPretopology P).toGrothendieck :=
  by
  ext X R
  rw [GrothendieckTopology.mem_over_iff]
  constructor
  · intro hR
    obtain ⟨𝒰, hle⟩ := exists_cover_of_mem_grothendieckTopology hR
    rw [mem_grothendieckTopology_iff] at hR
    letI (i : 𝒰.I₀) : (𝒰.X i).Over S := { hom := 𝒰.f i ≫ X.hom }
    letI : 𝒰.Over S :=
      { over := inferInstance
        isOver_map := fun i ↦ ⟨rfl⟩ }
    use 𝒰.toPresieveOver, ⟨𝒰, inferInstance, rfl⟩
    rwa [Cover.toPresieveOver_le_arrows_iff]
  · rintro ⟨T, ⟨𝒰, h, rfl⟩, hT⟩
    use Presieve.ofArrows 𝒰.X 𝒰.f, 𝒰.mem_pretopology
    rwa [Cover.toPresieveOver_le_arrows_iff] at hT

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