instFiniteCarrierCarrierCommRingCatFiberOfIsFinite

English

If f: X → Y is a finite morphism, then for every y ∈ Y the fiber X_y has finitely many points (the topological space underlying X_y is finite).

Русский

Если f: X → Y конечный морфизм, то для любой y ∈ Y фибра X_y содержит конечное число точек.

LaTeX

$$$\forall f:X\to Y\;[\operatorname{IsFinite}(f)],\ \forall y\in Y:\; \#|X_y|<\infty.$$$

Lean4

instance (f : X ⟶ Y) (y : Y) [IsFinite f] : Finite (f.fiber y) :=
  by
  have H : IsFinite (f.fiberToSpecResidueField y) := MorphismProperty.pullback_snd _ _ inferInstance
  have : IsArtinianRing Γ(f.fiber y, ⊤) :=
    @IsArtinianRing.of_finite (Y.residueField y) Γ(f.fiber y, ⊤) _ _ (show _ from _) _ _
      ((HasAffineProperty.iff_of_isAffine.mp H).2.comp
        (.of_surjective _ (Scheme.ΓSpecIso (Y.residueField y)).commRingCatIsoToRingEquiv.symm.surjective))
  exact .of_injective (β := PrimeSpectrum _) _ (f.fiber y).isoSpec.hom.homeomorph.injective

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