eq_isProper_inf_isAffineHom — Mathlib

English

The finite morphism predicate IsFinite is equal to the infimum of IsProper and IsAffineHom in the lattice of morphism properties.

Русский

Свойство IsFinite равно пересечению (в лаг) IsProper и IsAffineHom: IsFinite = IsProper ⊓ IsAffineHom.

LaTeX

$$@IsFinite = (@IsProper ⊓ @IsAffineHom : MorphismProperty _)$$

Lean4

theorem eq_isProper_inf_isAffineHom : @IsFinite = (@IsProper ⊓ @IsAffineHom : MorphismProperty _) :=
  by
  have : (@IsAffineHom ⊓ @IsSeparated : MorphismProperty _) = @IsAffineHom :=
    inf_eq_left.mpr fun _ _ _ _ ↦ inferInstance
  rw [inf_comm, isProper_eq, inf_assoc, ← inf_assoc, this, eq_inf, IsIntegralHom.eq_universallyClosed_inf_isAffineHom,
    inf_assoc, inf_left_comm]

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