English
The morphism 𝔸(n; S) ↓ S is integral if and only if either S or n is empty.
Русский
Гомоморфизм 𝔸(n; S) ↓ S интегрален тогда и только тогда, когда пусты либо S, либо n.
LaTeX
$$$IsIntegralHom\big(\mathbb{A}(n;S) \downarrow S\big) \iff IsEmpty\,S \lor IsEmpty\,n$$$
Lean4
theorem isIntegralHom_over_iff_isEmpty : IsIntegralHom (𝔸(n; S) ↘ S) ↔ IsEmpty S ∨ IsEmpty n :=
by
constructor
· intro h
cases isEmpty_or_nonempty S
· exact .inl ‹_›
refine .inr ?_
wlog hS : ∃ R, S = Spec R
· obtain ⟨x⟩ := ‹Nonempty S›
obtain ⟨y, hy⟩ := S.affineCover.covers x
exact
this (S.affineCover.X _)
(MorphismProperty.IsStableUnderBaseChange.of_isPullback (isPullback_map (S.affineCover.f _)) h) ⟨y⟩ ⟨_, rfl⟩
obtain ⟨R, rfl⟩ := hS
have : Nontrivial R :=
(subsingleton_or_nontrivial R).resolve_left fun H ↦
not_isEmpty_of_nonempty (Spec R) (inferInstanceAs (IsEmpty (PrimeSpectrum R)))
constructor
intro i
have := RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.isIntegral_respectsIso.{max u v}
rw [← MorphismProperty.cancel_left_of_respectsIso @IsIntegralHom (SpecIso n R).inv, SpecIso_inv_over,
HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom)] at h
obtain ⟨p : Polynomial R, hp, hp'⟩ :=
(MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty RingHom.IsIntegral)
(arrowIsoΓSpecOfIsAffine _)).mpr
h.2 (X i)
have : (rename fun _ ↦ i).comp (pUnitAlgEquiv.{_, v} _).symm.toAlgHom p = 0 := by simp [← hp', ← algebraMap_eq]
rw [AlgHom.comp_apply, map_eq_zero_iff _ (rename_injective _ (fun _ _ _ ↦ rfl))] at this
simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_coe, EmbeddingLike.map_eq_zero_iff] at this
simp [this] at hp
· rintro (_ | _) <;> infer_instance
