instLocallyOfFiniteTypeOfLocallyOfFinitePresentation

English

If a morphism is LocallyOfFinitePresentation, then it is LocallyOfFiniteType.

Русский

Если морфизм локально презентационен, то он локально конечного типа.

LaTeX

$$$\text{LocallyOfFinitePresentation}(f) \Rightarrow \text{LocallyOfFiniteType}(f).$$$

Lean4

instance {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] : LocallyOfFiniteType f :=
  by
  rw [HasRingHomProperty.eq_affineLocally @LocallyOfFinitePresentation] at hf
  rw [HasRingHomProperty.eq_affineLocally @LocallyOfFiniteType]
  refine affineLocally_le (fun hf ↦ ?_) f hf
  exact RingHom.FiniteType.of_finitePresentation hf

Похожие утверждения