of_pullback_fst_Spec_of_codescendsAlong

English

If P is stable under base-change and pullbacks, then P descends along pullback squares against a morphism f with P' in the configuration.

Русский

Если P устойчиво к базовым изменениям и к каноническим диагональным тождествам, то P спускается вдоль квадратов возвращающих по f с P' в конфигурации.

LaTeX

$$$[P'.RespectsIso]\\, [P'.IsStableUnderBaseChange] \\Rightarrow P.DescendsAlong (P' ⊓ @QuasiCompact)$$$

Lean4

theorem of_pullback_fst_Spec_of_codescendsAlong [P.RespectsIso] (hQQ' : RingHom.CodescendsAlong Q Q')
    (H₁ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' f.hom)
    (H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q f.hom) {R S T : CommRingCat.{u}}
    {f : Spec T ⟶ Spec R} {g : Spec S ⟶ Spec R} (h : P' f) (hf : P (pullback.fst f g)) : P g :=
  by
  obtain ⟨φ, rfl⟩ := Spec.map_surjective g
  obtain ⟨ψ, rfl⟩ := Spec.map_surjective f
  algebraize [φ.hom, ψ.hom]
  replace hf :
    P
      (pullback.fst (Spec.map <| CommRingCat.ofHom <| algebraMap R T)
        (Spec.map <| CommRingCat.ofHom <| algebraMap R S)) :=
    hf
  rw [H₂]
  refine hQQ'.algebraMap_tensorProduct (R := R) (S := T) (T := S) _ (H₁ h) ?_
  rwa [← pullbackSpecIso_hom_fst R T S, P.cancel_left_of_respectsIso, H₂] at hf

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