English
For an AlgHom f: R → A and a matrix M over R, f.mapMatrix(M.adjugate) = M.adjugate after applying f entrywise to M.
Русский
Для AlgHom f: R → A верно, что f.mapMatrix(M.adjugate) = adjugate(f.mapMatrix M).
LaTeX
$$$\operatorname{AlgHom}.mapMatrix(M).adjugate = \operatorname{AlgHom}.mapMatrix(M.adjugate)$$$
Lean4
theorem _root_.RingHom.map_adjugate {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S) (M : Matrix n n R) :
f.mapMatrix M.adjugate = Matrix.adjugate (f.mapMatrix M) :=
by
ext i k
have : Pi.single i (1 : S) = f ∘ Pi.single i 1 := by
rw [← f.map_one]
exact Pi.single_op (fun _ => f) (fun _ => f.map_zero) i (1 : R)
rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ← map_updateRow, ←
RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]
