property_coverMap_comp

Mathlib.AlgebraicGeometry.Morphisms.LocalClosure

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.sourceLocalClosure.property_coverMap_comp

English

If W contains identities and respects isomorphisms, then P is contained in the source local closure of P with respect to W.

Русский

Если W содержит идентичности и сохраняет изоморфизмы, то P ⊆ sourceLocalClosure W P.

LaTeX

$$P ≤ sourceLocalClosure W P$$

Lean4

theorem property_coverMap_comp {f : X ⟶ Y} (hf : sourceLocalClosure W P f) (i : hf.cover.I₀) : P (hf.cover.f i ≫ f) :=
  hf.choose_spec i

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

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

Разделы

Аффилиация

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