Local rank of the dual of a finite projective module

The linear dual of a finite projective module has the same rank at every prime of the base ring. This is the module-theoretic rank identity underlying preservation of rank by Cartier duality, including over disconnected and nonreduced bases.

The argument uses the scalar-extension evaluation equivalence from TauCeti.LinearAlgebra.Dual.BaseChange and Mathlib's dimension formula for linear duals.

@[simp]

theorem TauCeti.Module.rankAtStalk_dual (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Module.rankAtStalk (Module.Dual R M) = Module.rankAtStalk M

A finite projective module and its linear dual have the same rank at every prime.