instHasRingHomPropertyLocallyOfFiniteTypeFiniteType

English

LocallyOfFiniteType is stable under composition of morphisms.

Русский

LocallyOfFiniteType устойчива по композиции морфизмов.

LaTeX

$$$\text{LocallyOfFiniteType}(f) \land \text{LocallyOfFiniteType}(g) \Rightarrow \text{LocallyOfFiniteType}(f \circ g).$$$

Lean4

instance : HasRingHomProperty (@LocallyOfFiniteType) RingHom.FiniteType
    where
  isLocal_ringHomProperty := RingHom.finiteType_isLocal
  eq_affineLocally' := by
    ext X Y f
    rw [locallyOfFiniteType_iff, affineLocally_iff_affineOpens_le]

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