@[reducible, inline]

abbrev MorphismDefinitions.IsFiniteAlgebra (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [Algebra B A] : Prop

A B-algebra A is finite if A is a finitely generated B-module.

theorem MorphismDefinitions.isFiniteAlgebra_isIntegral (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [Algebra B A] [Module.Finite B A] : Algebra.IsIntegral B A

A finite algebra is integral.

theorem MorphismDefinitions.finite_morphism_isClosedMap {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] [Module.Finite B A] : IsClosedMap (PrimeSpectrum.comap (algebraMap B A))

A finite morphism of rings induces a closed map on prime spectra (Lec 3–4).

theorem MorphismDefinitions.finite_morphism_finite_fibers {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] [Module.Finite B A] (𝔭 : PrimeSpectrum B) : (PrimeSpectrum.comap (algebraMap B A) ⁻¹' {𝔭}).Finite

A finite morphism has finite fibers on prime spectra.

theorem MorphismDefinitions.finite_morphism_surjective_on_spec {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] [Module.Finite B A] (hinj : Function.Injective ⇑(algebraMap B A)) : Function.Surjective (PrimeSpectrum.comap (algebraMap B A))

A finite injective morphism of rings is surjective on prime spectra (Corollary 9).

theorem MorphismDefinitions.finite_morphism_fiber_finite_nonempty {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] [Module.Finite B A] (hinj : Function.Injective ⇑(algebraMap B A)) (𝔭 : PrimeSpectrum B) : (PrimeSpectrum.comap (algebraMap B A) ⁻¹' {𝔭}).Finite ∧ (PrimeSpectrum.comap (algebraMap B A) ⁻¹' {𝔭}).Nonempty

For a finite injective morphism, each fiber on prime spectra is finite and nonempty.

theorem MorphismDefinitions.finite_morphism_dim_eq {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] [Module.Finite B A] (hinj : Function.Injective ⇑(algebraMap B A)) : ringKrullDim A = ringKrullDim B

A finite injective morphism of rings preserves Krull dimension.