descendsAlong — Mathlib

English

Let P be a property stable under isomorphisms and base-change. If P' codescends along Q', then P descends along P'.

Русский

Пусть P устойчиво к изоморфизмам и базовым изменениям. Если P' кодоментируется по отношению к Q', то P спускается вдоль P'.

LaTeX

$$$[P.RespectsIso] \\Rightarrow (P'.CodescendsAlong Q Q') \\Rightarrow (P.DescendsAlong P')$$$

Lean4

/-- If `P` is local at the target, to show `P` descends along `P'` we may assume
the base to be affine. -/
theorem descendsAlong [IsZariskiLocalAtTarget P] [P'.IsStableUnderBaseChange]
    (H :
      ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R), P' f → P (pullback.fst f g) → P g) :
    P.DescendsAlong P' := by
  apply MorphismProperty.DescendsAlong.mk'
  introv h hf
  wlog hZ : ∃ R, Z = Spec R generalizing X Y Z
  · rw [IsZariskiLocalAtTarget.iff_of_openCover (P := P) Z.affineCover]
    intro i
    let ι := Z.affineCover.f i
    let e : pullback (pullback.snd f ι) (pullback.snd g ι) ≅ pullback (pullback.fst f g) (pullback.fst f ι) :=
      pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
        pullback.congrHom rfl pullback.condition.symm ≪≫
          (pullbackAssoc f g g ι).symm ≪≫
            pullback.congrHom pullback.condition.symm rfl ≪≫ (pullbackRightPullbackFstIso f ι (pullback.fst f g)).symm
    have heq :
      e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι) :=
      by apply pullback.hom_ext <;> simp [e, pullback.condition]
    refine this (f := pullback.snd f ι) ?_ ?_ ⟨_, rfl⟩
    · exact P'.pullback_snd _ _ h
    · change P (pullback.fst (pullback.snd f ι) (pullback.snd g ι))
      rw [← heq, P.cancel_left_of_respectsIso]
      exact
        AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback (iY := pullback.fst f ι)
          (CategoryTheory.IsPullback.of_hasPullback _ _) hf
  obtain ⟨R, rfl⟩ := hZ
  exact H f g h hf

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