Determinant transformation laws, and determinants of updated rows

Precomposing an alternating form of top degree with an endomorphism φ multiplies it by LinearMap.det φ, and — the direction that is actually used — a nonzero form merely known to be scaled by some d thereby identifies d as the determinant, without computing it, as soon as scalars cancel against nonzero vectors of the codomain (IsCancelMulZero R and Module.IsTorsionFree R N; see the implementation notes, where ω ≠ 0 alone is shown to be insufficient). This file records that law in three vocabularies: for an AlternatingMap indexed by a basis' index type, for an alternating bilinear form on a rank-two module, and for the standard-basis determinant form under matrix multiplication.

Mathlib's Module.Basis.det_comp is the case ω = b.det of the first statement. The step taken here is that every top-degree alternating form is a multiple of b.det (AlternatingMap.eq_basis_det_smulRight), so the same law holds for all of them; that is what makes the converse available for a form supplied by something other than a basis, such as a pairing.

The file also records one identity for the determinant of a matrix with one row replaced, alongside Mathlib's Matrix.det_updateRow_add and Matrix.det_updateRow_smul: Jacobi's formula in row form, that rescaling one row entry by entry along a fixed vector of factors and summing the results over the rows multiplies the determinant by the total of the factors.

Main results

• AlternatingMap.eq_basis_det_smulRight: ω = b.det.smulRight (ω b) for ω of top degree.
• AlternatingMap.compLinearMap_eq_det_smul: ω ∘ φ = det φ • ω for ω of top degree.
• LinearMap.det_eq_of_compLinearMap_eq_smul: if ω ≠ 0 and ω ∘ φ = d • ω then det φ = d, for R cancellative and N torsion-free.
• LinearMap.IsAlt.compl₁₂_self_eq_det_smul and LinearMap.det_eq_of_compl₁₂_self_eq_smul: the same two statements for an alternating bilinear form on a module of rank two.
• Matrix.detRowAlternating_mulVec: multiplication by a square matrix scales the standard-basis determinant form by the matrix determinant.
• Matrix.sum_det_updateRow_mul_row: Jacobi's formula for a determinant, in row form.
• Matrix.det_mul_column_intCast: scaling every row i of an integer matrix by d i multiplies the determinant by ∏ i, d i, over any commutative ring.
• LinearEquiv.det_ker_eq_bot_of_finrank_le_one: the determinant kernel is trivial in dimension at most one.

Implementation notes

The forms are valued in an arbitrary module N, not in R. Mathlib's AlternatingMap.eq_smul_basis_det is the N = R case of the first result here; the codomain plays no part in the argument, only the coordinates do, so the N-valued statement is what is proved.

The recovery statements need cancellation hypotheses, not just ω ≠ 0, and neither of the two assumed can be dropped:

• without IsCancelMulZero R: over R = ZMod 4, with N = R (which is torsion-free over itself), the form ω = 2 • b.det is nonzero and satisfies ω ∘ id = 3 • ω, while det id = 1;
• without Module.IsTorsionFree R N: over R = ℤ, with M = ℤ² and N = ZMod 2, the determinant form reduced mod 2, (x, y) ↦ x₀ y₁ - x₁ y₀, is nonzero and alternating, and φ = 3 • id scales it by 9, that is by 1, while det φ = 9.

IsCancelMulZero R and Module.IsTorsionFree R N are assumed for the recovery statements, and for nothing else; together they let a nonzero form, an element of a torsion-free module of alternating or bilinear maps, cancel from det φ • ω = d • ω.

None of the transformation laws stated for a basis is a simp lemma: the basis is a hypothesis and does not occur in the conclusion, so simp could not infer it.

The bilinear statements use LinearMap.IsAlt.toAlternatingMap to read an alternating bilinear form as an AlternatingMap on Fin 2.

Provenance

The four transformation and recovery laws are ported from the AINTLIB HasseWeil project (Apache-2.0), revision 513e83879e2f, file HasseWeil/WeilPairing/PairingDet.lean, declarations alternating_comp_eq_det_smul and det_eq_of_alternating_scaling. The source states them over a field, for a scalar-valued form, evaluated at a basis, and proves the first by expanding φ (b j) in coordinates; none of that is reproduced here. Matrix.detRowAlternating_mulVec predates that port and is not from the source.

theorem AlternatingMap.eq_basis_det_smulRight {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) (ω : M [⋀^ι]→ₗ[R] N) : ω = b.det.smulRight (ω ⇑b)

A top-degree alternating form is its basis determinant times its value on the basis. This is Mathlib's AlternatingMap.eq_smul_basis_det with the codomain an arbitrary module rather than R.

theorem AlternatingMap.compLinearMap_eq_det_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Finite ι] (b : Module.Basis ι R M) (ω : M [⋀^ι]→ₗ[R] N) (φ : M →ₗ[R] M) : ω.compLinearMap φ = LinearMap.det φ • ω

An endomorphism scales a top-degree alternating form by its determinant. Here ω is of top degree in the sense that its index type indexes a basis of M; that basis is a hypothesis and does not occur in the conclusion, which is an equality of alternating maps.

theorem LinearMap.det_eq_of_compLinearMap_eq_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Finite ι] [IsCancelMulZero R] [Module.IsTorsionFree R N] (b : Module.Basis ι R M) {ω : M [⋀^ι]→ₗ[R] N} (hω : ω ≠ 0) {φ : M →ₗ[R] M} {d : R} (h : ω.compLinearMap φ = d • ω) : LinearMap.det φ = d

The multiplier of a nonzero top-degree alternating form is the determinant. An endomorphism which scales ω by d has det φ = d; the scaling identifies the determinant without computing it, and only the one endomorphism is involved.

The cancellation hypotheses on R and N are required, not incidental: dropping either one leaves the multiplier of a nonzero ω ambiguous, as the two examples in the module docstring show.

theorem LinearMap.IsAlt.compl₁₂_self_eq_det_smul {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (b : Module.Basis (Fin 2) R M) {ω : M →ₗ[R] M →ₗ[R] N} (halt : ω.IsAlt) (φ : M →ₗ[R] M) : ω.compl₁₂ φ φ = LinearMap.det φ • ω

An endomorphism of a rank-two module scales an alternating bilinear form by its determinant. The basis is a hypothesis witnessing that the rank is two; it does not occur in the conclusion, which is an equality of bilinear maps.

theorem LinearMap.det_eq_of_compl₁₂_self_eq_smul {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsCancelMulZero R] [Module.IsTorsionFree R N] (b : Module.Basis (Fin 2) R M) {ω : M →ₗ[R] M →ₗ[R] N} (halt : ω.IsAlt) (hω : ω ≠ 0) {φ : M →ₗ[R] M} {d : R} (h : ω.compl₁₂ φ φ = d • ω) : LinearMap.det φ = d

The multiplier of a nonzero alternating bilinear form on a rank-two module is the determinant. This is the form the additivised Weil pairing supplies: its scaling by an isogeny's degree identifies that degree as a determinant.

As above, neither cancellation hypothesis can be dropped; the module docstring's ZMod 2 example is itself an alternating bilinear form on a rank-two module.

@[simp]

theorem LinearEquiv.det_ker_eq_bot_of_finrank_le_one {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (hV : Module.finrank R V ≤ 1) : LinearEquiv.det.ker = ⊥

The determinant kernel on a finite free module of rank at most one is trivial.

@[simp]

theorem Matrix.detRowAlternating_mulVec {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [CommRing R] (M : Matrix ι ι R) (v : ι → ι → R) : (detRowAlternating fun (i : ι) => M.mulVec (v i)) = M.det * detRowAlternating v

Multiplication by a square matrix scales the standard-basis determinant form by its determinant. This is AlternatingMap.compLinearMap_eq_det_smul at ω = (Pi.basisFun R ι).det, in matrix vocabulary.

theorem Matrix.sum_det_updateRow_mul_row {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : Type u_2} [CommRing R] (A : Matrix ι ι R) (d : ι → R) : ∑ k : ι, (A.updateRow k fun (j : ι) => d j * A k j).det = (∑ j : ι, d j) * A.det

Jacobi's formula for a determinant, in row form. Rescale one row of a matrix entry by entry along a fixed vector of factors, and sum the resulting determinants over the rows: the answer is the determinant multiplied by the total of the factors.

theorem Matrix.det_mul_column_intCast {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (d : n → R) (M : Matrix n n ℤ) : (of fun (i j : n) => d i * ↑(M i j)).det = (∏ i : n, d i) * ↑M.det

The determinant of a scaled integer matrix. Scaling every row i of an integer matrix M by d i, with the entries cast into a commutative ring R, multiplies the determinant by ∏ i, d i.