English
For a morphism f: X → Y, f is finite if and only if f is integral and locally of finite type.
Русский
Для морфизма f: X → Y верно: f конечен тогда и только тогда, когда f интегрально и локально конечного типа.
LaTeX
$$$\mathrm{IsFinite}(f) \;\iff\; (\mathrm{IsIntegralHom}(f) \wedge \mathrm{LocallyOfFiniteType}(f)).$$$
Lean4
theorem iff_isIntegralHom_and_locallyOfFiniteType : IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f :=
by
wlog hY : IsAffine Y
· rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
IsZariskiLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover,
IsZariskiLocalAtTarget.iff_of_openCover (P := @LocallyOfFiniteType) Y.affineCover]
simp_rw [this, forall_and]
rw [HasAffineProperty.iff_of_isAffine (P := @IsFinite), HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom),
RingHom.finite_iff_isIntegral_and_finiteType, ← and_assoc]
refine and_congr_right fun ⟨_, _⟩ ↦ (HasRingHomProperty.iff_of_isAffine (P := @LocallyOfFiniteType)).symm
