English
The finite morphism property is stable under base change and localization, and affine finiteness transfers to opposite opens and presheaves.
Русский
Свойство конечности морфизмов устойчиво к базовым изменениям и локализации; конечность сохраняется при переходе к противоположным открытым множествам и прецепламу.
LaTeX
$$$HasAffineProperty\\ IsFinite (affineAnd \\\\ (RingHom.Finite))$$$
Lean4
instance : HasAffineProperty @IsFinite (fun X _ f _ ↦ IsAffine X ∧ RingHom.Finite (f.appTop).hom) :=
by
change HasAffineProperty @IsFinite (affineAnd RingHom.Finite)
rw [HasAffineProperty.affineAnd_iff _ RingHom.finite_respectsIso RingHom.finite_localizationPreserves.away
RingHom.finite_ofLocalizationSpan]
simp [isFinite_iff]
