Invertible matrices over subalgebras

An invertible matrix over a commutative algebra comes from a subalgebra exactly when its entries and those of its inverse lie in that subalgebra. This distinguishes invertibility over the subalgebra from invertibility over the ambient algebra.

For the equalizer of an algebra endomorphism with the identity, the inverse-entry condition follows from the entry condition: an entrywise map is a group homomorphism, so it fixes the inverse of every matrix it fixes. Thus the general linear group over that equalizer maps onto the fixed subgroup of the endomorphism. These characteristic-free statements apply in particular to Frobenius endomorphisms of algebras over finite fields, including the zero ring.

Main results

• Matrix.GeneralLinearGroup.mem_range_map_val_iff: descent to a subalgebra is equivalent to membership of the entries of the matrix and its inverse.
• Matrix.GeneralLinearGroup.map_eq_self_iff_mem_equalizer: a matrix is fixed by an entrywise algebra endomorphism exactly when its entries lie in its equalizer with the identity. The base may be a commutative semiring.
• Matrix.GeneralLinearGroup.range_map_val_equalizer: the image of the general linear group over the equalizer subalgebra is the fixed subgroup of the entrywise endomorphism. A commutative ring base ensures that subalgebras carry the ring structure used by the entrywise map.

@[simp]

theorem Matrix.GeneralLinearGroup.mem_range_map_val_iff {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (S : Subalgebra R A) (g : GL ι A) : (∃ (h : GL ι ↥S), (map ↑S.val) h = g) ↔ (∀ (i j : ι), ↑g i j ∈ S) ∧ ∀ (i j : ι), ↑g⁻¹ i j ∈ S

Which invertible matrices come from a subalgebra: those whose entries, and whose inverse's entries, all lie in it. Over a subalgebra invertibility is a condition on the inverse rather than a consequence of the determinant being a unit of the ambient algebra, so the second clause cannot be dropped.

@[simp]

theorem Matrix.GeneralLinearGroup.map_eq_self_iff_mem_equalizer {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommRing A] [Algebra R A] (φ : A →ₐ[R] A) (g : GL ι A) : (map ↑φ) g = g ↔ ∀ (i j : ι), ↑g i j ∈ φ.equalizer (AlgHom.id R A)

An invertible matrix is fixed by an entrywise algebra endomorphism exactly when every one of its entries lies in the equalizer of that endomorphism with the identity.

theorem Matrix.GeneralLinearGroup.range_map_val_equalizer {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (φ : A →ₐ[R] A) : (map ↑(φ.equalizer (AlgHom.id R A)).val).range = TauCeti.fixedSubgroup (map ↑φ)

The invertible matrices fixed by an entrywise algebra endomorphism are exactly the ones coming from its equalizer subalgebra. The entries of a fixed matrix are fixed, and so are those of its inverse because the entrywise map is a group homomorphism, so a fixed matrix descends.

No characteristic hypothesis is used, so this also covers the q-power endomorphism of an arbitrary algebra over a finite field, where iterateFrobenius is unavailable because the zero ring has no exponential characteristic p.