theorem nakayama_determinant_form {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] (I : Ideal R) (hIM : I • ⊤ = ⊤) : ∃ (a : R), a - 1 ∈ I ∧ ∀ (m : M), a • m = 0

Determinant form of Nakayama's lemma (Lem 4, Lec 3): if I · M = M for a finitely generated module M, there exists a with a - 1 ∈ I annihilating M.

theorem nakayama_exists_identity_element {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] (I : Ideal R) (hIM : I • ⊤ = ⊤) : ∃ a ∈ I, ∀ (m : M), a • m = m

Identity-element form of Nakayama: under the same hypotheses, there is some a ∈ I acting as the identity on M.

theorem nakayama_ne_top_of_le_jacobson {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Nontrivial M] [Module.Finite R M] (I : Ideal R) (hI : I ≤ ⊥.jacobson) : I • ⊤ ≠ ⊤

Nakayama: if I is contained in the Jacobson radical and M is nontrivial, then I · M ≠ M.

theorem nakayama_subsingleton_of_le_jacobson {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] (I : Ideal R) (hIM : I • ⊤ = ⊤) (hIjac : I ≤ ⊥.jacobson) : Subsingleton M

Contrapositive form: if I · M = M with I in the Jacobson radical, then M is the zero module.

theorem finite_morphism_spec_surjective (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [Algebra B A] [Module.Finite B A] [FaithfulSMul B A] : Function.Surjective (PrimeSpectrum.comap (algebraMap B A))

A finite faithful algebra has surjective Spec (going-up applied to integral).

theorem finite_morphism_spec_surjective_of_ringHom {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] (f : B →+* A) (hfin : f.Finite) (hinj : Function.Injective ⇑f) : Function.Surjective (PrimeSpectrum.comap f)

Ring-hom version: an injective finite ring homomorphism is surjective on prime spectra.

theorem essential_nullstellensatz (k : Type u_1) (A : Type u_2) [Field k] [Field A] [Algebra k A] [Algebra.FiniteType k A] : Algebra.IsAlgebraic k A

Essential form of the Nullstellensatz: a field which is a finitely generated algebra over another field is algebraic over it.

theorem finite_of_finiteType_field (k : Type u_1) (A : Type u_2) [Field k] [Field A] [Algebra k A] [Algebra.FiniteType k A] : Module.Finite k A

A field that is finitely generated as a k-algebra is in fact a finite k-module.