English
If P has affine-local behavior and f: X → Y together with an affine open cover 𝒰 of Y and compatible pullbacks 𝒰', then the diagonal P.diagonal f holds.
Русский
Если свойство P локально аффинно, и имеется отображение f: X → Y вместе с аффинным открытым покрытием 𝒰 схемы Y и совместимыми вытягиваниями 𝒰', то диагональ P.diagonal f выполняется.
LaTeX
$$$P.diagonal(f)$$$
Lean4
theorem diagonal_of_openCover (P) {Q} [HasAffineProperty P Q] {X Y : Scheme.{u}} (f : X ⟶ Y)
(𝒰 : Scheme.OpenCover.{u} Y) [∀ i, IsAffine (𝒰.X i)] (𝒰' : ∀ i, Scheme.OpenCover.{u} (pullback f (𝒰.f i)))
[∀ i j, IsAffine ((𝒰' i).X j)] (h𝒰' : ∀ i j k, Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (𝒰.pullbackHom f i))) :
P.diagonal f := by
letI := isLocal_affineProperty P
let 𝒱 :=
(Scheme.Pullback.openCoverOfBase 𝒰 f f).bind fun i =>
Scheme.Pullback.openCoverOfLeftRight.{u} (𝒰' i) (𝒰' i) (pullback.snd _ _) (pullback.snd _ _)
have i1 : ∀ i, IsAffine (𝒱.X i) := fun i => by dsimp [𝒱]; infer_instance
apply of_openCover 𝒱
rintro ⟨i, j, k⟩
dsimp [𝒱]
convert
(Q.cancel_left_of_respectsIso
((pullbackDiagonalMapIso _ _ ((𝒰' i).f j) ((𝒰' i).f k)).inv ≫ pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) _ _)
(pullback.snd _ _)).mp
_ using
1
· simp
· ext1 <;> simp
· simp only [Category.assoc, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, Category.comp_id]
convert h𝒰' i j k
ext1 <;> simp [Scheme.Cover.pullbackHom]
