smallGrothendieckTopologyOfLE — Mathlib

English

The glued presheaf is isomorphic to the represented presheaf via the Yoneda glue map.

Русский

Склейка прешепа изоморфна представленному прешепу через карту клея Йонеда.

LaTeX

$$IsIso (yonedaGluedToSheaf hf)$$

Lean4

/-- If `P` and `Q` are morphism properties with `P ≤ Q`, this is the Grothendieck topology
induced via the forgetful functor `Q.Over ⊤ S ⥤ Over S` by the topology defined by `P`. -/
abbrev smallGrothendieckTopologyOfLE (hPQ : P ≤ Q) : GrothendieckTopology (Q.Over ⊤ S) :=
  letI : (MorphismProperty.Over.forget Q ⊤ S).LocallyCoverDense (overGrothendieckTopology P S) :=
    locallyCoverDense_of_le S hPQ
  (MorphismProperty.Over.forget Q ⊤ S).inducedTopology (S.overGrothendieckTopology P)

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