The adjugate of an invertible matrix

The adjugate of an invertible matrix is invertible, so Matrix.adjugate restricts to a map GL n R → GL n R. Its inverse is exhibited directly, without dividing by the determinant: adjugate is anti-multiplicative and sends 1 to 1, so adjugate g⁻¹ inverts adjugate g on the nose. That keeps the construction over an arbitrary commutative ring — no field, no det ≠ 0 side condition, and nothing to discharge at a call site.

Over a group of determinant-one matrices it is the inverse, and in size two it is an involution. Those are the two ingredients a Hecke-pair anti-involution needs from the adjugate; the anti-involution itself also requires stability of the group and the monoid under the map, which is proved where those objects live, not here.

Main definitions

• TauCeti.adjugateGL: the adjugate as a map GL n R → GL n R.

Main results

• TauCeti.adjugateGL_one, TauCeti.adjugateGL_mul: adj(1) = 1 and adj(gh) = adj(h) adj(g).
• TauCeti.adjugateGL_eq_inv: on determinant one, adj(g) = g⁻¹.
• TauCeti.adjugateGL_mapGL: on a special-linear image, adj(mapGL σ) = mapGL σ⁻¹.
• TauCeti.adjugateGL_adjugateGL: in size two, adj is an involution.
• Matrix.adjugate_eq_det_smul_inv: adj(A) = det A • A⁻¹ for A of unit determinant, at any finite size.
• Matrix.GeneralLinearGroup.adjugateGL_eq_scalar_mul_inv: adj(g) = (det g · I) * g⁻¹.

References

• Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck), Apache-2.0, HeckeRIngs/GL2/HeckeActionGeneral.lean at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, declarations GL_adjugate, GL_adjugate_val, GL_adjugate_mul, GL_adjugate_involutive and GL_adjugate_eq_inv_of_det_one. The source is stated for GL (Fin 2) ℚ and builds the element with a det ≠ 0 obligation; here the inverse is exhibited directly, which removes that obligation and generalises the statements to GL n R over a commutative ring.

def TauCeti.adjugateGL {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] (g : GL n R) : GL n R

The adjugate of an invertible matrix, again invertible.

The inverse is adjugate g⁻¹ rather than anything built from the determinant: adjugate is anti-multiplicative, so the two adjugates multiply to adjugate (g⁻¹ g) = adjugate 1 = 1.

Equations

• TauCeti.adjugateGL g = { val := (↑g).adjugate, inv := (↑g⁻¹).adjugate, val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem TauCeti.adjugateGL_val {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] (g : GL n R) : ↑(adjugateGL g) = (↑g).adjugate

@[simp]

theorem TauCeti.adjugateGL_one {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] : adjugateGL 1 = 1

The adjugate fixes the identity.

@[simp]

theorem TauCeti.adjugateGL_mul {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] (g h : GL n R) : adjugateGL (g * h) = adjugateGL h * adjugateGL g

The adjugate is anti-multiplicative, inherited entrywise from Matrix.adjugate.

theorem TauCeti.adjugateGL_eq_inv {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] {g : GL n R} (hg : (↑g).det = 1) : adjugateGL g = g⁻¹

On determinant one the adjugate is the inverse. This is what makes it restrict to a group of determinant-one matrices, where it is then an anti-automorphism.

theorem TauCeti.adjugateGL_mapGL {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] {S : Type u_3} [CommRing S] [Algebra R S] (σ : Matrix.SpecialLinearGroup n R) : adjugateGL ((Matrix.SpecialLinearGroup.mapGL S) σ) = (Matrix.SpecialLinearGroup.mapGL S) σ⁻¹

Adjugate is inversion on a special-linear image. An element of SL n R has determinant one in every R-algebra S, so adjugateGL is inversion on its image, and mapGL S is a monoid map. This is adjugateGL_eq_inv in the form its consumers meet: the determinant hypothesis is discharged once here rather than at each call site.

theorem TauCeti.adjugateGL_adjugateGL {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] (h2 : Fintype.card n = 2) (g : GL n R) : adjugateGL (adjugateGL g) = g

In size two the adjugate is an involution. adjugate squares to det ^ (card n - 2) • id, and the size-two hypothesis makes that exponent vanish.

theorem Matrix.adjugate_eq_det_smul_inv {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] {A : Matrix n n R} (hA : IsUnit A.det) : A.adjugate = A.det • A⁻¹

The adjugate is the determinant times the inverse: adj A = det A • A⁻¹, whenever the determinant is a unit. Matrix.inv_def read backwards, at any finite size.

theorem Matrix.GeneralLinearGroup.adjugateGL_eq_scalar_mul_inv {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] (g : GL n R) : TauCeti.adjugateGL g = (scalar n) (det g) * g⁻¹

The adjugate of an invertible matrix is its inverse rescaled by the determinant: adj g = (det g · I) * g⁻¹, in GL n R. Writing it as a product with a scalar matrix is what lets a multiplicative action be split along the adjugate — the weight-k slash is, in TauCeti/NumberTheory/ModularForms/SlashAdjugate.lean.

In size two, and only there, the adjugate is an involution (adjugateGL_adjugateGL); it is that specialisation that the modular literature calls the main involution and writes α^ι.

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB @ 6d87d596a537, Apache-2.0), projects/LeanModularForms/LeanModularForms/HeckeRIngs/GL2/AdjointTheory.lean, whose peterssonAdj is adjugateGL at GL (Fin 2) ℝ and records the same identity in its docstring ("α† = det(α) · α⁻¹ = adjugate(α)").