English
If P is Zariski-local both at the source and at the target, there is a transfer to a canonical ring-hom property on Spec maps.
Русский
Если P является зарисковским локальным и в источнике, и в целевом, существует перенос к каноническому свойству кольцевых гомоморфизмов на Spec-картах.
LaTeX
$$of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget$$
Lean4
theorem of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget [IsZariskiLocalAtTarget P] [IsZariskiLocalAtSource P] :
HasRingHomProperty P (fun f ↦ P (Spec.map (CommRingCat.ofHom f)))
where
isLocal_ringHomProperty := isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget P
eq_affineLocally' := by
let Q := affineLocally (fun f ↦ P (Spec.map (CommRingCat.ofHom f)))
have : HasRingHomProperty Q (fun f ↦ P (Spec.map (CommRingCat.ofHom f))) :=
⟨isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget P, rfl⟩
change P = Q
ext X Y f
wlog hY : ∃ R, Y = Spec R generalizing X Y
· rw [IsZariskiLocalAtTarget.iff_of_openCover (P := P) Y.affineCover,
IsZariskiLocalAtTarget.iff_of_openCover (P := Q) Y.affineCover]
refine forall_congr' fun _ ↦ this _ ⟨_, rfl⟩
obtain ⟨S, rfl⟩ := hY
wlog hX : ∃ R, X = Spec R generalizing X
· rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) X.affineCover,
IsZariskiLocalAtSource.iff_of_openCover (P := Q) X.affineCover]
refine forall_congr' fun _ ↦ this _ ⟨_, rfl⟩
obtain ⟨R, rfl⟩ := hX
obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f := ⟨_, Spec.map_preimage _⟩
rw [HasRingHomProperty.Spec_iff (P := Q)]
rfl
