Determinants of endomorphisms of finite projective modules

Mathlib's LinearMap.det is the determinant of an endomorphism of a module with a finite basis, and is 1 on every other module. This file defines the determinant LinearMap.projectiveDet : Module.End R M →* R of an endomorphism of a finite projective module M, that is, of a finite locally free module, which need not be free.

Choose a free module F of finite rank with linear maps π : F →ₗ[R] M and σ : M →ₗ[R] F such that π ∘ₗ σ = id. Then F is the internal direct sum of the image σ(M) ≅ M and the kernel of π, and the endomorphism σ ∘ₗ f ∘ₗ π + (1 - σ ∘ₗ π) of F is f on the first summand and the identity on the second. Its determinant does not depend on F, π and σ (LinearMap.projectiveDet_eq_det_of_comp_eq_id), by the Weinstein–Aronszajn identity det (1 + X ∘ₗ Y) = det (1 + Y ∘ₗ X) for linear maps X and Y between free modules of finite rank (LinearMap.det_one_add_comp_comm). This determinant is projectiveDet f. Its image in a localization R_𝔭, over which M_𝔭 is free, is the determinant of the matrix of f_𝔭 in a basis (LinearMap.projectiveDet_baseChange and LinearMap.projectiveDet_eq_det), so it agrees with the determinant defined through local trivializations.

The determinant is multiplicative, agrees with LinearMap.det on free modules, commutes with arbitrary base change, is invariant under conjugation by linear equivalences, and detects invertibility. It is the determinant underlying the norm of a finite locally free algebra, Algebra.projectiveNorm.

Main definitions

• LinearMap.projectiveDet: the determinant of an endomorphism of a finite projective module.

Main results

• LinearMap.projectiveDet_eq_det_of_comp_eq_id: projectiveDet f is the determinant of σ ∘ₗ f ∘ₗ π + (1 - σ ∘ₗ π) for every splitting π ∘ₗ σ = id through a free module of finite rank.
• LinearMap.projectiveDet_comp and LinearMap.projectiveDet_id: the determinant is multiplicative.
• LinearMap.projectiveDet_eq_det: on a free module of finite rank, projectiveDet is LinearMap.det.
• LinearMap.projectiveDet_baseChange: the determinant commutes with base change along any ring homomorphism.
• LinearMap.projectiveDet_conj: the determinant is invariant under conjugation by a linear equivalence.
• LinearMap.isUnit_iff_isUnit_projectiveDet: an endomorphism is invertible if and only if its determinant is a unit.

References

• O. Goldman, Determinants in projective modules, Nagoya Math. J. 18 (1961), 27–36.
• The Stacks Project, Tag 0BIF (the norm of a finite locally free algebra).

noncomputable def LinearMap.projectiveDet {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Module.End R M →* R

The determinant of an endomorphism f of a finite projective module M: for a free module F of finite rank with π : F →ₗ[R] M and σ : M →ₗ[R] F such that π ∘ₗ σ = id, it is the determinant of the endomorphism σ ∘ₗ f ∘ₗ π + (1 - σ ∘ₗ π) of F, which is f on σ(M) and the identity on ker π. It does not depend on the choice of F, π and σ (projectiveDet_eq_det_of_comp_eq_id), and it is LinearMap.det when M is free (projectiveDet_eq_det).

theorem LinearMap.projectiveDet_eq_det_of_comp_eq_id {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {F : Type u_4} [AddCommGroup F] [Module R F] [Module.Free R F] [Module.Finite R F] (π : F →ₗ[R] M) (σ : M →ₗ[R] F) (h : π ∘ₗ σ = id) (f : Module.End R M) : projectiveDet f = LinearMap.det (σ ∘ₗ f ∘ₗ π + (1 - σ ∘ₗ π))

The determinant projectiveDet f is the determinant of σ ∘ₗ f ∘ₗ π + (1 - σ ∘ₗ π), for any free module F of finite rank with linear maps π : F →ₗ[R] M and σ : M →ₗ[R] F such that π ∘ₗ σ = id.

@[simp]

theorem LinearMap.projectiveDet_comp {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (f g : Module.End R M) : projectiveDet (f ∘ₗ g) = projectiveDet f * projectiveDet g

The determinant of a composite is the product of the determinants.

@[simp]

theorem LinearMap.projectiveDet_id {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : projectiveDet id = 1

The determinant of the identity is 1.

@[simp]

theorem LinearMap.projectiveDet_baseChange {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (A : Type u_4) [CommRing A] [Algebra R A] (f : Module.End R M) : projectiveDet (baseChange A f) = (algebraMap R A) (projectiveDet f)

The determinant of an endomorphism of a finite projective module commutes with base change: the determinant of f.baseChange A is the image of the determinant of f.

@[simp]

theorem LinearMap.projectiveDet_conj {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Projective R M] [Module.Finite R N] [Module.Projective R N] (f : Module.End R M) (e : M ≃ₗ[R] N) : projectiveDet (↑e ∘ₗ f ∘ₗ ↑e.symm) = projectiveDet f

The determinant of an endomorphism of a finite projective module is invariant under conjugation by a linear equivalence.

theorem LinearMap.isUnit_iff_isUnit_projectiveDet {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (f : Module.End R M) : IsUnit f ↔ IsUnit (projectiveDet f)

An endomorphism of a finite projective module is invertible if and only if its determinant is a unit.

@[simp]

theorem LinearMap.projectiveDet_eq_det {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] (f : Module.End R M) : projectiveDet f = LinearMap.det f

On a free module of finite rank, projectiveDet is the determinant LinearMap.det.