Dimensions over a field of modules over a finite algebra, computed locally

Let A be a finite algebra over a field k. Then A is Artinian, hence the product of its finitely many localizations A_q at primes, so every A-module M is the product of the A_q ⊗[A] M, and its k-dimension is the sum of theirs (TauCeti.Module.finrank_eq_finsum_finrank_localization_tensorProduct). For a quotient A ⧸ 𝔞 the factors are the quotients A_q ⧸ 𝔞 A_q (Ideal.finrank_quotient_eq_finsum).

The second half of the file is a local-to-global criterion for the additivity dim A = dim (A ⧸ 𝔞) + dim (A ⧸ 𝔟). Over any finite-dimensional k-algebra L, multiplication by a identifies L ⧸ Ann(a) with the principal ideal (a), so dim L = dim (L ⧸ (a)) + dim (L ⧸ Ann(a)) (TauCeti.finrank_quotient_span_singleton_add_finrank_quotient_annihilator). Hence if, at every prime q of A, the ideal 𝔞 A_q is generated by an element a whose annihilator is 𝔟 A_q, then summing over the primes gives dim (A ⧸ 𝔞) + dim (A ⧸ 𝔟) = dim A (TauCeti.finrank_quotient_add_finrank_quotient_of_forall).

Geometrically, for effective Cartier divisors D and E with local equations a and b, the ideal of D in D + E is locally (a) ⊆ 𝒪 ⧸ (ab), whose annihilator is (b), the ideal of E. The criterion therefore says that the degree of a finite divisor D + E over a field is the sum of the degrees of D and E.

References

• Stacks Project, Tag 00JA: an Artinian ring is the product of its localizations at its maximal ideals.

theorem TauCeti.Module.finrank_eq_finsum_finrank_localization_tensorProduct (k : Type u_1) {A : Type u_2} (M : Type u_3) [Field k] [CommRing A] [Algebra k A] [Module.Finite k A] [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] [Module.Finite A M] : Module.finrank k M = ∑ᶠ (q : PrimeSpectrum A), Module.finrank k (TensorProduct A (Localization.AtPrime q.asIdeal) M)

Over a finite algebra A over a field k, the k-dimension of a finite A-module M is the sum, over the finitely many primes q of A, of the k-dimensions of the localizations A_q ⊗[A] M.

theorem Ideal.finrank_quotient_eq_finsum (k : Type u_1) {A : Type u_2} [Field k] [CommRing A] [Algebra k A] [Module.Finite k A] (𝔞 : Ideal A) : Module.finrank k (A ⧸ 𝔞) = ∑ᶠ (q : PrimeSpectrum A), Module.finrank k (Localization.AtPrime q.asIdeal ⧸ map (algebraMap A (Localization.AtPrime q.asIdeal)) 𝔞)

Over a finite algebra A over a field k, the k-dimension of a quotient A ⧸ 𝔞 is the sum, over the primes q of A, of the k-dimensions of the local quotients A_q ⧸ 𝔞 A_q.

theorem TauCeti.finrank_quotient_span_singleton_add_finrank_quotient_annihilator {k : Type u_1} {L : Type u_2} [Field k] [CommRing L] [Algebra k L] [Module.Finite k L] (a : L) : Module.finrank k (L ⧸ Ideal.span {a}) + Module.finrank k (L ⧸ Submodule.annihilator (Ideal.span {a})) = Module.finrank k L

Multiplication by a splits a finite-dimensional algebra. Over a finite-dimensional commutative k-algebra L, multiplication by a identifies L ⧸ Ann(a) with the principal ideal (a), so dim L = dim (L ⧸ (a)) + dim (L ⧸ Ann(a)).

theorem TauCeti.finrank_quotient_add_finrank_quotient_of_forall {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] [Module.Finite k A] (𝔞 𝔟 : Ideal A) (L : PrimeSpectrum A → Type u_3) [(q : PrimeSpectrum A) → CommRing (L q)] [(q : PrimeSpectrum A) → Algebra A (L q)] [∀ (q : PrimeSpectrum A), IsLocalization.AtPrime (L q) q.asIdeal] (h : ∀ (q : PrimeSpectrum A), ∃ (a : L q), Ideal.map (algebraMap A (L q)) 𝔞 = Ideal.span {a} ∧ Ideal.map (algebraMap A (L q)) 𝔟 = Submodule.annihilator (Ideal.span {a})) : Module.finrank k (A ⧸ 𝔞) + Module.finrank k (A ⧸ 𝔟) = Module.finrank k A

A local criterion for additivity of dimensions. Let A be a finite algebra over a field k, and let 𝔞 and 𝔟 be ideals of A. Suppose that for every prime q of A, in some localization L q of A at q, the ideal 𝔞 L q is generated by an element a whose annihilator is 𝔟 L q. Then dim (A ⧸ 𝔞) + dim (A ⧸ 𝔟) = dim A.