iff_of_isAffine — Mathlib

English

If Y is affine, then P f holds if and only if Q f holds.

Русский

Если Y аффинна, то P f эквивалентно Q f.

LaTeX

$$$[IsAffine Y] \Rightarrow (P f \iff Q f)$$$

Lean4

theorem iff_of_isAffine [IsAffine Y] : P f ↔ Q f :=
  by
  letI := isLocal_affineProperty P
  haveI : ∀ i, IsAffine ((Scheme.coverOfIsIso (P := @IsOpenImmersion) (𝟙 Y)).X i) := fun i => by dsimp; infer_instance
  rw [iff_of_openCover (P := P) (Scheme.coverOfIsIso.{0} (𝟙 Y))]
  trans Q (pullback.snd f (𝟙 _))
  · exact ⟨fun H => H PUnit.unit, fun H _ => H⟩
  rw [← Category.comp_id (pullback.snd _ _), ← pullback.condition, Q.cancel_left_of_respectsIso]

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