English
If P has a HasOfPostcomp property for IsOpenImmersion and respects postcomposition, then the diagonal of P also inherits this property at the source.
Русский
Если P имеет свойство HasOfPostcomp для IsOpenImmersion и сохраняет посткомпозицию, диагональ этого свойства наследуется у источника.
LaTeX
$$IsZariskiLocalAtSource diagonal(P)$$
Lean4
instance (P : MorphismProperty Scheme) [P.HasOfPostcompProperty @IsOpenImmersion] [P.RespectsRight @IsOpenImmersion]
[IsZariskiLocalAtSource P] : IsZariskiLocalAtSource P.diagonal :=
by
let g {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) :=
pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) (by simp) (by simp)
refine IsZariskiLocalAtSource.mk' (fun {X Y} f U hf ↦ ?_) (fun {X Y} f {ι} U hU hf ↦ ?_)
· change P _
apply P.of_postcomp (W' := @IsOpenImmersion) (pullback.diagonal (U.ι ≫ f)) (g f U) inferInstance
rw [← pullback.comp_diagonal]
apply IsZariskiLocalAtSource.comp
exact hf
· change P _
refine IsZariskiLocalAtSource.of_iSup_eq_top U hU fun i ↦ ?_
rw [pullback.comp_diagonal]
exact RespectsRight.postcomp (P := P) (Q := @IsOpenImmersion) (g _ _) inferInstance _ (hf i)
