smallGrothendieckTopology

Mathlib.AlgebraicGeometry.Sites.Small

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.smallGrothendieckTopology

Lean4

/-- The Grothendieck topology on the category of schemes over `S` with `P` induced by `P`, i.e.
coverings are simply surjective families. This is the induced topology by the topology on `S`
defined by `P` via the inclusion `P.Over ⊤ S ⥤ Over S`.

This is a special case of `smallGrothendieckTopologyOfLE` for the case `P = Q`. -/
abbrev smallGrothendieckTopology : GrothendieckTopology (P.Over ⊤ S) :=
  (MorphismProperty.Over.forget P ⊤ S).inducedTopology (S.overGrothendieckTopology P)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru