grothendieckTopology_eq_toGrothendieck_pretopology

English

If the morphism property P is multiplicative and stable under base change, then the Grothendieck topology generated by P equals the Grothendieck topology induced by the pretopology associated to P.

Русский

Если свойство морфизмов P является мультипликативным и сохраняется при базовом изменении, то топология Гротендик, порождаемая P, совпадает с топологией Гротендик, порождаемой претопологией, связанной с P.

LaTeX

$$$P\text{.grothendieckTopology} = P\text{.pretopology.toGrothendieck}$$$

Lean4

/-- If `P` is also multiplicative, the topology induced by `P` is the topology induced by the
pretopology induced by `P`. -/
theorem grothendieckTopology_eq_toGrothendieck_pretopology [P.IsMultiplicative] :
    P.grothendieckTopology = P.pretopology.toGrothendieck := by
  rw [grothendieckTopology, coverage_eq_toCoverage_pretopology, Pretopology.toGrothendieck_toCoverage]

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