Invertible modules and line bundles

This file proves the standard characterization of invertible modules as finite locally free modules of rank one. This fills the corresponding TODO in mathlib's Mathlib/RingTheory/PicardGroup.lean.

Main definitions

• Module.IsLocallyFreeRankOne R M: M is finite projective and has rank one at every stalk.
• Module.IsRankOnePairing R M: the rank-one identity for the evaluation pairing.

Main results

• Module.invertible_iff_isLocallyFreeRankOne: invertible modules are exactly the finite locally free modules of rank one.
• Module.IsLocallyFreeRankOne.isRankOnePairing: a line bundle satisfies the rank-one pairing identity.
• Module.IsLocallyFreeRankOne.bilinMap_eq_zero_of_map_self_eq_zero: an alternating bilinear map out of a line bundle vanishes.
• Module.isRankOnePairing_of_invertible: the pairing identity for mathlib's invertible modules.

Proof idea

For the converse, choose a finite dual frame mᵢ, φᵢ for the projective module. Rank one at every stalk gives the identity φ(x)ψ(y) = φ(y)ψ(x). The trace of the frame is one, and consequently every elementary tensor satisfies

φ ⊗ x = φ(x) • ∑ᵢ φᵢ ⊗ mᵢ.

Thus contraction with the evaluation pairing is bijective, which is precisely mathlib's definition of Module.Invertible.

References

• [Stacks, Tag 00NX] The Stacks Project, Finite projective modules.
• [Stacks, Tag 0B8I] The Stacks Project, Invertible modules.

def Module.IsLocallyFreeRankOne (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] : Prop

An R-module is locally free of rank one if it is finite projective and its localization at every prime has rank one.

The finite-projective clauses are the algebraic form of finite local freeness; the stalk rank is mathlib's Module.rankAtStalk.

Equations

• Module.IsLocallyFreeRankOne R M = (Module.Finite R M ∧ Module.Projective R M ∧ Module.rankAtStalk M = 1)

def Module.IsRankOnePairing (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] : Prop

The evaluation pairing of M has the rank-one pairing identity if φ(x) ψ(y) = φ(y) ψ(x) for all functionals and vectors.

Equations

• Module.IsRankOnePairing R M = ∀ (φ ψ : Module.Dual R M) (x y : M), φ x * ψ y = φ y * ψ x

theorem Module.isRankOnePairing_of_linearEquiv {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (e : M ≃ₗ[R] R) : IsRankOnePairing R M

A module isomorphic to the base ring has the rank-one pairing identity.

theorem Module.isRankOnePairing_self {R : Type u} [CommRing R] : IsRankOnePairing R R

The base ring itself has the rank-one pairing identity.

theorem Module.IsLocallyFreeRankOne.isRankOnePairing {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (h : IsLocallyFreeRankOne R M) : IsRankOnePairing R M

A finite locally free module of rank one has the rank-one pairing identity.

theorem Module.IsLocallyFreeRankOne.bilinMap_eq_zero_of_map_self_eq_zero {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type u_1} [AddCommGroup N] [Module R N] (h : IsLocallyFreeRankOne R M) (B : LinearMap.BilinMap R M N) (hB : ∀ (x : M), (B x) x = 0) : B = 0

Every alternating bilinear map out of a line bundle vanishes. Equivalently, the second exterior power of a line bundle is zero.

theorem Module.invertible_iff_isLocallyFreeRankOne {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] : Module.Invertible R M ↔ IsLocallyFreeRankOne R M

An R-module is invertible if and only if it is finite locally free of rank one.

This is the module-theoretic characterization of line bundles; see Stacks, Tag 0B8I.

theorem Module.isRankOnePairing_of_invertible {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Invertible R M] : IsRankOnePairing R M

An invertible module satisfies the rank-one identity for its evaluation pairing.