eq_iInf — Mathlib

English

IsLocalIso is the infimum of all P with ContainsIdentities and IsZariskiLocalAtSource.

Русский

IsLocalIso есть infimum над всеми P, которые содержат идентичности и являются локальными по источнику.

LaTeX

$$$ IsLocalIso = \bigwedge_{P} (P.ContainsIdentities) (IsZariskiLocalAtSource P), P $$$

Lean4

/-- `IsLocalIso` is the weakest source-Zariski-local property containing identities. -/
theorem eq_iInf :
    @IsLocalIso = ⨅ (P : MorphismProperty Scheme.{u}) (_ : P.ContainsIdentities) (_ : IsZariskiLocalAtSource P), P :=
  by
  refine le_antisymm ?_ ?_
  · simp only [le_iInf_iff]
    apply le_of_isZariskiLocalAtSource
  · refine iInf_le_of_le @IsLocalIso (iInf_le_of_le inferInstance (iInf_le _ ?_))
    infer_instance

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