theorem prop27_isProper (k : Type u) [Field k] {X Y : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec (CommRingCat.of k))] [Y.Over (AlgebraicGeometry.Spec (CommRingCat.of k))] [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec (CommRingCat.of k))] [AlgebraicGeometry.IsProper (Y ↘ AlgebraicGeometry.Spec (CommRingCat.of k))] (f : X ⟶ Y) [AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec (CommRingCat.of k))] : AlgebraicGeometry.IsProper f

A morphism between two proper k-schemes that is itself compatible with the structure maps is proper.

theorem lemma_29_toNormalization_isIso (k : Type u) [Field k] {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsIntegral Y] [X.Over (AlgebraicGeometry.Spec (CommRingCat.of k))] [Y.Over (AlgebraicGeometry.Spec (CommRingCat.of k))] [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec (CommRingCat.of k))] [AlgebraicGeometry.IsProper (Y ↘ AlgebraicGeometry.Spec (CommRingCat.of k))] (f : X ⟶ Y) [AlgebraicGeometry.IsDominant f] [AlgebraicGeometry.IsProper f] : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.toNormalization f)

Lemma 29: for a dominant proper morphism of integral schemes, the induced map to the normalization of Y is an isomorphism.

theorem prop_28_fromNormalization_isFinite (k : Type u) [Field k] {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsIntegral Y] [X.Over (AlgebraicGeometry.Spec (CommRingCat.of k))] [Y.Over (AlgebraicGeometry.Spec (CommRingCat.of k))] [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec (CommRingCat.of k))] [AlgebraicGeometry.IsProper (Y ↘ AlgebraicGeometry.Spec (CommRingCat.of k))] (f : X ⟶ Y) [AlgebraicGeometry.IsDominant f] [AlgebraicGeometry.IsProper f] : AlgebraicGeometry.IsFinite (AlgebraicGeometry.Scheme.Hom.fromNormalization f)

Proposition 28: for a dominant proper morphism of integral schemes, the canonical map from the normalization back to Y is finite.

theorem prop27_nonconstant_map_finite {k : Type u} [Field k] {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsIntegral Y] [X.Over (AlgebraicGeometry.Spec (CommRingCat.of k))] [Y.Over (AlgebraicGeometry.Spec (CommRingCat.of k))] [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec (CommRingCat.of k))] [AlgebraicGeometry.IsProper (Y ↘ AlgebraicGeometry.Spec (CommRingCat.of k))] (_hdimX : topologicalKrullDim ↥X = 1) (_hdimY : topologicalKrullDim ↥Y = 1) (f : X ⟶ Y) [AlgebraicGeometry.IsDominant f] [AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec (CommRingCat.of k))] : AlgebraicGeometry.IsFinite f

Proposition 27: a non-constant (dominant) morphism between irreducible proper curves over k is finite.