feat: affine isomorphisms between spaces of affine maps (leanprover-community#35998)

These isomorphisms are analogous to `LinearEquiv.arrowCongr` and `LinearEquiv.congrLeft`.

Author: gasparattila

Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

@@ -613,6 +613,129 @@ theorem ofLinearEquiv_trans_ofLinearEquiv (A B : V ≃ₗ[k] V) (p₀ p₁ p₂
 
 end ofLinearEquiv
 
+section arrowCongrEquiv
+
+variable (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₃ ≃ᵃ[k] P₄)
+
+/-- Affine isomorphisms between the domains and codomains of two spaces of affine maps give a
+bijection between the two function spaces.
+
+See `AffineEquiv.arrowCongr` and `AffineEquiv.arrowCongrₗ` for the affine and linear versions of
+this bijection. -/
+def arrowCongrEquiv : (P₁ →ᵃ[k] P₃) ≃ (P₂ →ᵃ[k] P₄) where
+  toFun f := e₂.toAffineMap.comp <| f.comp e₁.symm.toAffineMap
+  invFun f := e₂.symm.toAffineMap.comp <| f.comp e₁.toAffineMap
+  left_inv _ := by ext; simp
+  right_inv _ := by ext; simp
+
+@[simp]
+theorem arrowCongrEquiv_apply (f : P₁ →ᵃ[k] P₃) (x : P₂) :
+    e₁.arrowCongrEquiv e₂ f x = e₂ (f (e₁.symm x)) :=
+  rfl
+
+@[simp]
+theorem arrowCongrEquiv_symm_apply (f : P₂ →ᵃ[k] P₄) (x : P₁) :
+    (e₁.arrowCongrEquiv e₂).symm f x = e₂.symm (f (e₁ x)) :=
+  rfl
+
+end arrowCongrEquiv
+
+section CommRing
+
+variable {R : Type*} [CommRing R] [Module R V₁] [Module R V₂] [Module R V₃] [Module R V₄]
+
+section arrowCongrₗ
+
+variable (e₁ : P₁ ≃ᵃ[R] P₂) (e₂ : V₃ ≃ₗ[R] V₄)
+
+/-- An affine isomorphism between the domains and a linear isomorphism between the codomains of two
+spaces of affine maps give a linear isomorphism between the two function spaces.
+
+See also `AffineEquiv.arrowCongrEquiv` and `AffineEquiv.arrowCongr`. -/
+def arrowCongrₗ : (P₁ →ᵃ[R] V₃) ≃ₗ[R] (P₂ →ᵃ[R] V₄) where
+  __ := e₁.arrowCongrEquiv e₂.toAffineEquiv
+  map_add' _ _ := by ext; simp
+  map_smul' _ _ := by ext; simp
+
+@[simp]
+theorem arrowCongrₗ_apply (f : P₁ →ᵃ[R] V₃) (x : P₂) :
+    e₁.arrowCongrₗ e₂ f x = e₂ (f (e₁.symm x)) :=
+  rfl
+
+@[simp]
+theorem arrowCongrₗ_symm_apply (f : P₂ →ᵃ[R] V₄) (x : P₁) :
+    (e₁.arrowCongrₗ e₂).symm f x = e₂.symm (f (e₁ x)) :=
+  rfl
+
+end arrowCongrₗ
+
+section arrowCongr
+
+variable (e₁ : P₁ ≃ᵃ[R] P₂) (e₂ : P₃ ≃ᵃ[R] P₄)
+
+/-- Affine isomorphisms between the domains and codomains of two spaces of affine maps give an
+affine isomorphism between the two function spaces.
+
+See also `AffineEquiv.arrowCongrEquiv` and `AffineEquiv.arrowCongrₗ`. -/
+@[simps linear]
+def arrowCongr : (P₁ →ᵃ[R] P₃) ≃ᵃ[R] (P₂ →ᵃ[R] P₄) where
+  __ := e₁.arrowCongrEquiv e₂
+  linear := e₁.arrowCongrₗ e₂.linear
+  map_vadd' _ _ := by ext; simp
+
+@[simp]
+theorem arrowCongr_apply (f : P₁ →ᵃ[R] P₃) (x : P₂) :
+    e₁.arrowCongr e₂ f x = e₂ (f (e₁.symm x)) :=
+  rfl
+
+@[simp]
+theorem arrowCongr_symm_apply (f : P₂ →ᵃ[R] P₄) (x : P₁) :
+    (e₁.arrowCongr e₂).symm f x = e₂.symm (f (e₁ x)) :=
+  rfl
+
+end arrowCongr
+
+end CommRing
+
+section congrLeft
+
+variable (R W : Type*) [Ring R] [AddCommGroup W] [Module k W] [Module R W] [SMulCommClass k R W]
+  (e : P₁ ≃ᵃ[k] P₂)
+
+/-- An affine isomorphism between the domains of affine spaces induces a linear isomorphism over
+another ring between the two function spaces. -/
+def congrLeftₗ : (P₁ →ᵃ[k] W) ≃ₗ[R] (P₂ →ᵃ[k] W) where
+  __ := e.arrowCongrEquiv (.refl k W)
+  map_add' _ _ := by ext; simp
+  map_smul' _ _ := by ext; simp
+
+@[simp]
+theorem congrLeftₗ_apply (f : P₁ →ᵃ[k] W) (x : P₂) : e.congrLeftₗ R W f x = f (e.symm x) :=
+  rfl
+
+@[simp]
+theorem congrLeftₗ_symm_apply (f : P₂ →ᵃ[k] W) (x : P₁) : (e.congrLeftₗ R W).symm f x = f (e x) :=
+  rfl
+
+variable {W} (Q : Type*) [AddTorsor W Q]
+
+/-- An affine isomorphism between the domains of affine spaces induces an affine isomorphism over
+another ring between the two function spaces. -/
+def congrLeft : (P₁ →ᵃ[k] Q) ≃ᵃ[R] (P₂ →ᵃ[k] Q) where
+  __ := e.arrowCongrEquiv (.refl k Q)
+  linear := e.congrLeftₗ R W
+  map_vadd' _ _ := by ext; simp
+
+@[simp]
+theorem congrLeft_apply (f : P₁ →ᵃ[k] Q) (x : P₂) : e.congrLeft R Q f x = f (e.symm x) :=
+  rfl
+
+@[simp]
+theorem congrLeft_symm_apply (f : P₂ →ᵃ[k] Q) (x : P₁) : (e.congrLeft R Q).symm f x = f (e x) :=
+  rfl
+
+end congrLeft
+
 end AffineEquiv
 
 namespace AffineMap