Determinant transformation laws, evaluation, 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. It also identifies evaluation of the row determinant form on a family of linear functionals with the determinant of their evaluation matrix. Ideal membership of these determinants extends from a set of rows to its linear span.

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.

It also records facts used to compute ideals of maximal minors: the determinant in a product basis of a block-diagonal family, and of a family that becomes block diagonal after a permutation, and Cramer's rule for an endomorphism of a free module of finite rank. On a free module of rank one, every endomorphism is multiplication by its determinant.

Finally, it records the Weinstein–Aronszajn identity det (1 + X ∘ₗ Y) = det (1 + Y ∘ₗ X) for linear maps X and Y between two free modules of finite rank, possibly of different ranks.

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.
• LinearMap.det_eq_of_compl₁₂_self_eq_smul_of_separatingLeft: the recovery statement over any commutative ring, for a left-separating form.
• Matrix.detRowAlternating_mulVec: multiplication by a square matrix scales the standard-basis determinant form by the matrix determinant.
• Matrix.detRowAlternating_pi_apply: evaluating the row determinant form on a family of linear functionals gives the determinant of their evaluation matrix.
• Matrix.detRowAlternating_compLinearMap_pi_apply: the same evaluation in multilinear-map vocabulary after precomposition with the family of functionals.
• TauCeti.det_mem_of_mem_span: ideal membership of evaluation determinants extends from a set of rows to its linear span.
• 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.
• LinearMap.det_one_add_comp_comm: the Weinstein–Aronszajn identity det (1 + X ∘ₗ Y) = det (1 + Y ∘ₗ X) for linear maps between free modules of finite rank.
• LinearEquiv.det_eq_pow_of_forall_eq_smul: an automorphism acting as multiplication by a unit c has determinant c ^ finrank R V.
• LinearEquiv.det_ker_eq_bot_of_finrank_le_one: the determinant kernel is trivial in dimension at most one.
• Module.Basis.prod_det_sumElim: the determinant in a product basis of a family split between the two factors is the product of the two determinants.
• Module.Basis.exists_prod_det_eq_sign_smul_mul: the same up to sign for a family with exactly as many members in the first factor as the rank of the first factor.
• Module.Basis.det_smul_smul_vecCons: rescaling the first two of three vectors by r and r' multiplies their determinant by r * r'.
• Module.Basis.det_equivFun_symm_trans_equivFun: the coordinate change from a basis b to a basis b' has determinant b'.det b.
• Module.Basis.det_map_eq_det_toMatrix: evaluating b'.det on the image b.map e of a basis b under a linear equivalence e gives the determinant of LinearMap.toMatrix b b' e.
• LinearMap.det_smul_mem_range: Cramer's rule, det φ • x ∈ range φ.
• LinearMap.apply_eq_det_smul_of_finrank_eq_one: on a free module of rank one, an endomorphism is multiplication by its determinant.

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 these 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 • ω. A left-separating form needs neither: a scalar killing it kills a basis vector, so vanishes, and LinearMap.det_eq_of_compl₁₂_self_eq_smul_of_separatingLeft holds over every commutative ring. The examples above are not left-separating: 2 • b.det pairs 2 • b 0 to zero, and the reduced determinant form pairs 2 • e₀ to zero.

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, nor is the left-separating recovery statement.

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 Module.Basis.prod_det_sumElim {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι'] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (v : ι → M) (v' : ι' → M') : (b.prod b').det (Sum.elim (⇑(LinearMap.inl R M M') ∘ v) (⇑(LinearMap.inr R M M') ∘ v')) = b.det v * b'.det v'

The determinant in a product basis of a family whose first arguments lie in the first factor and whose last arguments lie in the second factor is the product of the two determinants.

theorem Module.Basis.exists_prod_det_eq_sign_smul_mul {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι'] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (w : ι ⊕ ι' → M × M') (P : ι ⊕ ι' → Prop) [DecidablePred P] (hcard : Fintype.card { i : ι ⊕ ι' // P i } = Fintype.card ι) (h₁ : ∀ (i : ι ⊕ ι'), P i → (w i).2 = 0) (h₂ : ∀ (i : ι ⊕ ι'), ¬P i → (w i).1 = 0) : ∃ (σ : Equiv.Perm (ι ⊕ ι')), (b.prod b').det w = Equiv.Perm.sign σ • ((b.det fun (k : ι) => (w (σ (Sum.inl k))).1) * b'.det fun (l : ι') => (w (σ (Sum.inr l))).2)

If the members of a family satisfying P lie in the first factor, the others lie in the second factor, and exactly card ι members satisfy P, then, after a permutation σ moving the former to the front, the determinant of the family in a product basis is, up to the sign of σ, the product of the determinants of the two blocks of components.

theorem Module.Basis.det_smul_smul_vecCons {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (b : Basis (Fin 3) R M) (r r' : R) (u w d : M) : b.det ![r • u, r' • w, d] = r * r' * b.det ![u, w, d]

Rescaling the first two of three vectors by r and r' multiplies their determinant in a basis by r * r'.

theorem Module.Basis.det_equivFun_symm_trans_equivFun {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Fintype ι] [DecidableEq ι] [CommRing R] [AddCommGroup M] [Module R M] (b b' : Basis ι R M) : ↑(LinearEquiv.det (b.equivFun.symm ≪≫ₗ b'.equivFun)) = b'.det ⇑b

The coordinate change from the basis b to the basis b', which sends the coordinates x of ∑ i, x i • b i in b to its coordinates in b', has determinant b'.det b.

theorem Module.Basis.det_map_eq_det_toMatrix {ι : Type u_1} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [Fintype ι] [DecidableEq ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι R M') (e : M ≃ₗ[R] M') : b'.det ⇑(b.map e) = ((LinearMap.toMatrix b b') ↑e).det

Evaluating the determinant form of a basis b' on the image b.map e of a basis b under a linear equivalence e gives the determinant of the matrix of e with respect to b and b'.

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.

theorem LinearMap.det_eq_of_compl₁₂_self_eq_smul_of_separatingLeft {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) (hω : ω.SeparatingLeft) {φ : M →ₗ[R] M} {d : R} (h : ω.compl₁₂ φ φ = d • ω) : LinearMap.det φ = d

The multiplier of a left-separating alternating bilinear form on a rank-two module is the determinant, over any commutative ring. Left separation of ω takes the place of the cancellation hypotheses of LinearMap.det_eq_of_compl₁₂_self_eq_smul; this is the form that applies to the Weil pairing on N-torsion, a module over ZMod N, which is not a domain for composite N.

theorem LinearMap.det_one_add_comp_comm {R : Type u_2} [CommRing R] {F : Type u_5} {F' : Type u_6} [AddCommGroup F] [Module R F] [Module.Free R F] [Module.Finite R F] [AddCommGroup F'] [Module R F'] [Module.Free R F'] [Module.Finite R F'] (X : F' →ₗ[R] F) (Y : F →ₗ[R] F') : LinearMap.det (1 + X ∘ₗ Y) = LinearMap.det (1 + Y ∘ₗ X)

The Weinstein–Aronszajn identity for linear maps: for linear maps X : F' →ₗ[R] F and Y : F →ₗ[R] F' between free modules of finite rank, det (1 + X ∘ₗ Y) = det (1 + Y ∘ₗ X). This is Mathlib's Matrix.det_one_add_mul_comm, read through the matrices of X and Y in bases.

theorem LinearMap.det_smul_mem_range {R : Type u_2} [CommRing R] {F : Type u_5} [AddCommGroup F] [Module R F] [Module.Free R F] [Module.Finite R F] (φ : F →ₗ[R] F) (x : F) : LinearMap.det φ • x ∈ φ.range

Cramer's rule for an endomorphism. The determinant of an endomorphism φ of a free module of finite rank multiplies every vector into the range of φ: det φ • x = φ (adj φ x), for the adjugate adj φ of φ.

theorem LinearMap.apply_eq_det_smul_of_finrank_eq_one {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] (hM : Module.finrank R M = 1) (f : M →ₗ[R] M) (x : M) : f x = LinearMap.det f • x

An endomorphism of a free module of rank one is multiplication by its determinant.

theorem LinearEquiv.det_eq_pow_of_forall_eq_smul {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] (e : V ≃ₗ[R] V) (c : Rˣ) (h : ∀ (x : V), e x = c • x) : LinearEquiv.det e = c ^ Module.finrank R V

An automorphism of a free module acting as multiplication by a unit c has determinant c ^ finrank R V.

@[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_pi_apply {ι : Type u_1} {R : Type u_2} {F : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] [AddCommGroup F] [Module R F] (f : ι → Module.Dual R F) (v : ι → F) : (detRowAlternating fun (i : ι) => (LinearMap.pi f) (v i)) = (of fun (i j : ι) => (f j) (v i)).det

Evaluating the row determinant form after a family of linear functionals gives the matrix of those functionals evaluated on the input vectors.

theorem Matrix.detRowAlternating_compLinearMap_pi_apply {ι : Type u_1} {R : Type u_2} {F : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] [AddCommGroup F] [Module R F] (f : ι → Module.Dual R F) (v : ι → F) : ↑(detRowAlternating.compLinearMap (LinearMap.pi f)) v = (of fun (i j : ι) => (f j) (v i)).det

The multilinear form obtained by precomposing the row determinant with a family of linear functionals evaluates to the determinant of their evaluation matrix.

theorem TauCeti.det_mem_of_mem_span {ι : Type u_1} {R : Type u_2} {F : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] [AddCommGroup F] [Module R F] {s : Set F} {I : Ideal R} (f : ι → Module.Dual R F) {v : ι → F} (hv : ∀ (i : ι), v i ∈ Submodule.span R s) (h : ∀ (w : ι → F), (∀ (i : ι), w i ∈ s) → (Matrix.of fun (i j : ι) => (f j) (w i)).det ∈ I) : (Matrix.of fun (i j : ι) => (f j) (v i)).det ∈ I

If an ideal contains all evaluation determinants whose rows lie in a set, it also contains those whose rows lie in the linear span of that set. The row and functional families may be indexed by any finite type.

@[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.