The maximal ideal and the cotangent space of a quotient of a local ring

Let π : Q → A be a surjective homomorphism of local rings. Then π maps 𝔪_Q onto 𝔪_A, and an element of Q maps into 𝔪_A² exactly when it lies in ker π + 𝔪_Q². Consequently lifts to Q of a basis of the cotangent space 𝔪_A / 𝔪_A² span 𝔪_Q modulo ker π + 𝔪_Q², and they are linearly independent modulo it.

For a local homomorphism R → S with S local and an ideal J of R, the induced map R ⧸ J → S ⧸ J S is again local. Dividing both sides of a local homomorphism by an ideal of the base, as in inductions on the dimension of the base, therefore stays among local homomorphisms. When J is the maximal ideal of R and generates the maximal ideal of S, this map is the residue field extension, whose degree is then the rank of a finite free S.

Main results

• TauCeti.IsLocalRing.apply_mem_maximalIdeal_sq_iff: π a ∈ 𝔪_A² if and only if a ∈ ker π + 𝔪_Q².
• TauCeti.IsLocalRing.not_isPrincipal_maximalIdeal_of_ker_le_sq: if ker π ≤ 𝔪_Q² and no single element spans 𝔪_Q modulo 𝔪_Q², then 𝔪_A is not principal.
• TauCeti.IsLocalRing.maximalIdeal_quotient_eq_span_range: if 𝔪_Q = J + (yⱼ), then the images of the yⱼ generate the maximal ideal of Q ⧸ J.
• TauCeti.IsLocalRing.exists_lift_finBasis_cotangentSpace: lifts to Q of a basis of the cotangent space of A.
• Ideal.Quotient.isLocalHom_algebraMap_quotient_map_quotient: R ⧸ J → S ⧸ J S is a local homomorphism when R → S is one and S is local.
• TauCeti.IsLocalRing.finrank_residueField_eq_finrank: if S is finite free over R and 𝔪_R S = 𝔪_S, the residue field extension has degree [S : R], by Mathlib's IsLocalRing.finrank_quotient_map.

theorem TauCeti.IsLocalRing.apply_mem_maximalIdeal_sq_iff {Q : Type u_1} {A : Type u_2} [CommRing Q] [IsLocalRing Q] [CommRing A] [IsLocalRing A] {π : Q →+* A} (hπ : Function.Surjective ⇑π) (a : Q) : π a ∈ IsLocalRing.maximalIdeal A ^ 2 ↔ a ∈ RingHom.ker π ⊔ IsLocalRing.maximalIdeal Q ^ 2

Along a surjective homomorphism of local rings π : Q → A, an element a maps into 𝔪_A² if and only if it lies in ker π + 𝔪_Q².

theorem TauCeti.IsLocalRing.not_isPrincipal_maximalIdeal_of_ker_le_sq {Q : Type u_1} {A : Type u_2} [CommRing Q] [IsLocalRing Q] [CommRing A] [IsLocalRing A] {π : Q →+* A} (hπ : Function.Surjective ⇑π) (hker : RingHom.ker π ≤ IsLocalRing.maximalIdeal Q ^ 2) (h : ∀ z ∈ IsLocalRing.maximalIdeal Q, ¬IsLocalRing.maximalIdeal Q ≤ Ideal.span {z} ⊔ IsLocalRing.maximalIdeal Q ^ 2) : ¬Submodule.IsPrincipal (IsLocalRing.maximalIdeal A)

Along a surjective homomorphism of local rings π : Q → A with ker π ≤ 𝔪_Q², the maximal ideal of A is not principal as soon as no single element of 𝔪_Q spans 𝔪_Q modulo 𝔪_Q²: a generator π z of 𝔪_A would give 𝔪_Q ≤ (z) + ker π ≤ (z) + 𝔪_Q².

theorem TauCeti.IsLocalRing.maximalIdeal_quotient_eq_span_range {Q : Type u_1} [CommRing Q] [IsLocalRing Q] {κ : Type u_3} {J : Ideal Q} [IsLocalRing (Q ⧸ J)] {y : κ → Q} (h : IsLocalRing.maximalIdeal Q = J ⊔ Ideal.span (Set.range y)) : IsLocalRing.maximalIdeal (Q ⧸ J) = Ideal.span (Set.range (⇑(Ideal.Quotient.mk J) ∘ y))

If the maximal ideal of Q is J + (yⱼ), then the images of the yⱼ generate the maximal ideal of the local ring Q ⧸ J.

theorem TauCeti.IsLocalRing.exists_lift_finBasis_cotangentSpace {Q : Type u_1} {A : Type u_2} [CommRing Q] [IsLocalRing Q] [CommRing A] [IsLocalRing A] (hfg : (IsLocalRing.maximalIdeal Q).FG) {π : Q →+* A} (hπ : Function.Surjective ⇑π) : ∃ (y : Fin (Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.CotangentSpace A)) → Q), (∀ (j : Fin (Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.CotangentSpace A))), y j ∈ IsLocalRing.maximalIdeal Q) ∧ IsLocalRing.maximalIdeal Q ≤ Ideal.span (Set.range y) ⊔ (RingHom.ker π ⊔ IsLocalRing.maximalIdeal Q ^ 2) ∧ ∀ (c : Fin (Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.CotangentSpace A)) → Q), ∑ j : Fin (Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.CotangentSpace A)), c j * y j ∈ RingHom.ker π ⊔ IsLocalRing.maximalIdeal Q ^ 2 → ∀ (j : Fin (Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.CotangentSpace A))), c j ∈ IsLocalRing.maximalIdeal Q

Lifts of a basis of the cotangent space of a quotient. Let π : Q → A be a surjective homomorphism of local rings, where 𝔪_Q is finitely generated. Then there are lifts y : Fin e → Q of a basis of 𝔪_A / 𝔪_A², where e is its dimension. They lie in 𝔪_Q, span 𝔪_Q modulo ker π + 𝔪_Q², and are linearly independent modulo it: a combination ∑ cⱼ yⱼ lies in ker π + 𝔪_Q² only if every cⱼ ∈ 𝔪_Q.

instance Ideal.Quotient.isLocalHom_algebraMap_quotient_map_quotient {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] (J : Ideal R) : IsLocalHom (algebraMap (R ⧸ J) (S ⧸ map (algebraMap R S) J))

For a local homomorphism R → S to a local ring and an ideal J of R, the induced homomorphism R ⧸ J → S ⧸ J S is local. The ring R need not be local.

theorem TauCeti.IsLocalRing.finrank_residueField_eq_finrank {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [Module.Free R S] [Module.Finite R S] (h : Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) = IsLocalRing.maximalIdeal S) : Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) = Module.finrank R S

Residue degree of a finite free extension in which the maximal ideal stays maximal. If S is a finite free extension of the local ring R and the maximal ideal of R generates the maximal ideal of S, then the residue field extension has degree [S : R].

The proof is adapted from that of Mathlib's IsLocalRing.finrank_eq_finrank_residueField, the étale special case, and goes through Mathlib's IsLocalRing.finrank_quotient_map.