affineAnd_apply

Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.affineAnd_apply

English

If Q respects isomorphisms, then affineAnd Q also respects isomorphisms.

Русский

Если Q сохраняет изоморфизмы, то affineAnd Q также сохраняет изоморфизмы.

LaTeX

$$affineAnd_respectsIso (hP) : (affineAnd Q).toProperty.RespectsIso$$

Lean4

@[simp]
theorem affineAnd_apply {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffine Y] : affineAnd Q f ↔ IsAffine X ∧ Q (f.appTop).hom :=
  Iff.rfl

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

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

Разделы

Аффилиация

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