Intertwiners of linear automorphisms

A linear map f : V →ₗ[K] W intertwines automorphisms a of V and b of W when f ∘ a = b ∘ f. This is the heterogeneous form of SemiconjBy: source and target live in different modules, so the relation is not a statement inside one monoid and Mathlib's SemiconjBy API does not apply to it.

Main declarations

• LinearMap.GeneralLinearGroup.commute_ofLinearEquiv_iff: conversion from linear equivalences to the general linear group preserves and reflects commutation.
• LinearMap.GeneralLinearGroup.comp_inv_eq_of_comp_eq: an intertwiner of two automorphisms also intertwines their inverses.

theorem LinearMap.GeneralLinearGroup.commute_ofLinearEquiv_iff {K : Type u} {V : Type v} [Semiring K] [AddCommMonoid V] [Module K V] (f g : V ≃ₗ[K] V) : Commute (ofLinearEquiv f) (ofLinearEquiv g) ↔ Commute f g

Two linear equivalences commute if and only if their images in the general linear group commute.

theorem LinearMap.GeneralLinearGroup.comp_inv_eq_of_comp_eq {K : Type u} {V : Type v} {W : Type w} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (f : V →ₗ[K] W) (a : GeneralLinearGroup K V) (b : GeneralLinearGroup K W) (hab : f ∘ₗ ↑a = ↑b ∘ₗ f) : f ∘ₗ ↑a⁻¹ = ↑b⁻¹ ∘ₗ f

Intertwining passes to inverses. If f intertwines the automorphisms a and b, then it intertwines a⁻¹ and b⁻¹.