English
For finite n, the morphism 𝔸(n; S) ↓ S has Locally of Finite Presentation property (LFP) in the over-S setting.
Русский
Для конечного n отображение 𝔸(n; S) ↓ S обладает локально конечной презентацией в надS контексте.
LaTeX
$$$[Finite\\ n]\\Rightarrow LocallyOfFinitePresentation\\big(\\mathbb{A}(n; S) \\downarrow S\\big).$$$
Lean4
instance [Finite n] : LocallyOfFinitePresentation (𝔸(n; S) ↘ S) :=
MorphismProperty.pullback_fst _ _ <|
by
have := isIso_of_isTerminal specULiftZIsTerminal.{max u v} terminalIsTerminal (terminal.from _)
rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C)),
MorphismProperty.cancel_right_of_respectsIso (P := @LocallyOfFinitePresentation),
HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation), RingHom.FinitePresentation]
convert (inferInstanceAs (Algebra.FinitePresentation (ULift ℤ) ℤ[n]))
exact Algebra.algebra_ext _ _ fun _ ↦ rfl
