sigmaDesc — Mathlib

English

If P is local on the source, then P is preserved under forming Sigma-descents: if each f_i has P, then the canonical map Sigma.desc f has P.

Русский

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

LaTeX

$$$\forall {X : Scheme}, \forall {ι : Type v} [LowLevel.{u} ι], \forall {Y : ι \to Scheme}, {f : (\,i: ι) \to Y i \to X}, (\forall i, P(f i)) \Rightarrow P(\Sigma.desc f).$$$

Lean4

theorem sigmaDesc {X : Scheme.{u}} {ι : Type v} [Small.{u} ι] {Y : ι → Scheme.{u}} {f : ∀ i, Y i ⟶ X}
    (hf : ∀ i, P (f i)) : P (Sigma.desc f) :=
  by
  rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (Scheme.IsLocallyDirected.openCover _)]
  exact fun i ↦ by simp [hf]

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