feat(linear_algebra/affine_space/affine_equiv): isomorphism with the units (#10798)

This adds:
* `affine_equiv.equiv_units_affine_map` (the main point in this PR)
* `affine_map.linear_hom`
* `affine_equiv.linear_hom`
* `simps` configuration for `affine_equiv`. In order to makes `simp` happy, we adjust the order of the implicit variables to all lemmas in this file, so that they match the order of the arguments to `affine_equiv`.

The new definition can be used to majorly golf `homothety_units_mul_hom`

Author: eric-wieser

src/linear_algebra/affine_space/affine_equiv.lean

@@ -23,6 +23,9 @@ We define the following equivalences:
   `category_theory` convention (apply `e`, then `e'`), not the convention used in function
   composition and compositions of bundled morphisms.
 
+We equip `affine_equiv k P P` with a `group` structure with multiplication corresponding to
+composition in `affine_equiv.group`.
+
 ## Tags
 
 affine space, affine equivalence
@@ -45,7 +48,7 @@ structure affine_equiv (k P₁ P₂ : Type*) {V₁ V₂ : Type*} [ring k]
 
 notation P₁ ` ≃ᵃ[`:25 k:25 `] `:0 P₂:0 := affine_equiv k P₁ P₂
 
-variables {k V₁ V₂ V₃ V₄ P₁ P₂ P₃ P₄ : Type*} [ring k]
+variables {k P₁ P₂ P₃ P₄ V₁ V₂ V₃ V₄ : Type*} [ring k]
   [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁]
   [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂]
   [add_comm_group V₃] [module k V₃] [add_torsor V₃ P₃]
@@ -162,6 +165,15 @@ def mk' (e : P₁ → P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ p' :
 
 @[simp] lemma symm_linear (e : P₁ ≃ᵃ[k] P₂) : e.linear.symm = e.symm.linear := rfl
 
+/-- See Note [custom simps projection] -/
+def simps.apply (e : P₁ ≃ᵃ[k] P₂) : P₁ → P₂ := e
+
+/-- See Note [custom simps projection] -/
+def simps.symm_apply (e : P₁ ≃ᵃ[k] P₂) : P₂ → P₁ := e.symm
+
+initialize_simps_projections affine_equiv
+  (to_equiv_to_fun → apply, to_equiv_inv_fun → symm_apply, linear → linear as_prefix, -to_equiv)
+
 protected lemma bijective (e : P₁ ≃ᵃ[k] P₂) : bijective e := e.to_equiv.bijective
 protected lemma surjective (e : P₁ ≃ᵃ[k] P₂) : surjective e := e.to_equiv.surjective
 protected lemma injective (e : P₁ ≃ᵃ[k] P₂) : injective e := e.to_equiv.injective
@@ -242,21 +254,39 @@ lemma mul_def (e e' : P₁ ≃ᵃ[k] P₁) : e * e' = e'.trans e := rfl
 
 lemma inv_def (e : P₁ ≃ᵃ[k] P₁) : e⁻¹ = e.symm := rfl
 
+/-- `affine_equiv.linear` on automorphisms is a `monoid_hom`. -/
+@[simps] def linear_hom : (P₁ ≃ᵃ[k] P₁) →* (V₁ ≃ₗ[k] V₁) :=
+{ to_fun := linear,
+  map_one' := rfl,
+  map_mul' := λ _ _, rfl }
+
+/-- The group of `affine_equiv`s are equivalent to the group of units of `affine_map`.
+
+This is the affine version of `linear_map.general_linear_group.general_linear_equiv`. -/
+@[simps]
+def equiv_units_affine_map : (P₁ ≃ᵃ[k] P₁) ≃* units (P₁ →ᵃ[k] P₁) :=
+{ to_fun := λ e, ⟨e, e.symm, congr_arg coe e.symm_trans_self, congr_arg coe e.self_trans_symm⟩,
+  inv_fun := λ u,
+  { to_fun := (u : P₁ →ᵃ[k] P₁), inv_fun := (↑(u⁻¹) : P₁ →ᵃ[k] P₁),
+    left_inv := affine_map.congr_fun u.inv_mul,
+    right_inv := affine_map.congr_fun u.mul_inv,
+    linear := linear_map.general_linear_group.general_linear_equiv _ _ $
+      units.map (by exact affine_map.linear_hom) u,
+    map_vadd' := λ _ _, (u : P₁ →ᵃ[k] P₁).map_vadd _ _ },
+  left_inv := λ e, affine_equiv.ext $ λ x, rfl,
+  right_inv := λ u, units.ext $ affine_map.ext $ λ x, rfl,
+  map_mul' := λ e₁ e₂, rfl }
+
 variable (k)
 
 /-- The map `v ↦ v +ᵥ b` as an affine equivalence between a module `V` and an affine space `P` with
 tangent space `V`. -/
+@[simps]
 def vadd_const (b : P₁) : V₁ ≃ᵃ[k] P₁ :=
 { to_equiv := equiv.vadd_const b,
   linear := linear_equiv.refl _ _,
   map_vadd' := λ p v, add_vadd _ _ _ }
 
-@[simp] lemma linear_vadd_const (b : P₁) : (vadd_const k b).linear = linear_equiv.refl k V₁ := rfl
-
-@[simp] lemma vadd_const_apply (b : P₁) (v : V₁) : vadd_const k b v = v +ᵥ b := rfl
-
-@[simp] lemma vadd_const_symm_apply (b p : P₁) : (vadd_const k b).symm p = p -ᵥ b := rfl
-
 /-- `p' ↦ p -ᵥ p'` as an equivalence. -/
 def const_vsub (p : P₁) : P₁ ≃ᵃ[k] V₁ :=
 { to_equiv := equiv.const_vsub p,
@@ -270,17 +300,12 @@ def const_vsub (p : P₁) : P₁ ≃ᵃ[k] V₁ :=
 variable (P₁)
 
 /-- The map `p ↦ v +ᵥ p` as an affine automorphism of an affine space. -/
+@[simps]
 def const_vadd (v : V₁) : P₁ ≃ᵃ[k] P₁ :=
 { to_equiv := equiv.const_vadd P₁ v,
   linear := linear_equiv.refl _ _,
   map_vadd' := λ p w, vadd_comm _ _ _ }
 
-@[simp] lemma linear_const_vadd (v : V₁) : (const_vadd k P₁ v).linear = linear_equiv.refl _ _ := rfl
-
-@[simp] lemma const_vadd_apply (v : V₁) (p : P₁) : const_vadd k P₁ v p = v +ᵥ p := rfl
-
-@[simp] lemma const_vadd_symm_apply (v : V₁) (p : P₁) : (const_vadd k P₁ v).symm p = -v +ᵥ p := rfl
-
 section homothety
 
 omit V₁
@@ -291,21 +316,7 @@ include V
 /-- Fixing a point in affine space, homothety about this point gives a group homomorphism from (the
 centre of) the units of the scalars into the group of affine equivalences. -/
 def homothety_units_mul_hom (p : P) : units R →* P ≃ᵃ[R] P :=
-{ to_fun   := λ t,
-  { to_fun    := affine_map.homothety p (t : R),
-    inv_fun   := affine_map.homothety p (↑t⁻¹ : R),
-    left_inv  := λ p, by simp [← affine_map.comp_apply, ← affine_map.homothety_mul],
-    right_inv := λ p, by simp [← affine_map.comp_apply, ← affine_map.homothety_mul],
-    linear    :=
-    { inv_fun   := linear_map.lsmul R V (↑t⁻¹ : R),
-      left_inv  := λ v, by simp [smul_smul],
-      right_inv := λ v, by simp [smul_smul],
-      .. linear_map.lsmul R V t, },
-    map_vadd' := λ p v, by simp only [vadd_vsub_assoc, smul_add, add_vadd, affine_map.coe_line_map,
-      affine_map.homothety_eq_line_map, equiv.coe_fn_mk, linear_equiv.coe_mk,
-      linear_map.lsmul_apply, linear_map.to_fun_eq_coe], },
-  map_one' := by { ext, simp, },
-  map_mul' := λ t₁ t₂, by { ext, simp [← affine_map.comp_apply, ← affine_map.homothety_mul], }, }
+equiv_units_affine_map.symm.to_monoid_hom.comp $ units.map (affine_map.homothety_hom p)
 
 @[simp] lemma coe_homothety_units_mul_hom_apply (p : P) (t : units R) :
   (homothety_units_mul_hom p t : P → P) = affine_map.homothety p (t : R) :=
@@ -318,7 +329,7 @@ rfl
 @[simp] lemma coe_homothety_units_mul_hom_eq_homothety_hom_coe (p : P) :
   (coe : (P ≃ᵃ[R] P) → P →ᵃ[R] P) ∘ homothety_units_mul_hom p =
   (affine_map.homothety_hom p) ∘ (coe : units R → R) :=
-by { ext, simp, }
+funext $ λ _, rfl
 
 end homothety
 

src/linear_algebra/affine_space/affine_map.lean

@@ -306,6 +306,12 @@ instance : monoid (P1 →ᵃ[k] P1) :=
 @[simp] lemma coe_mul (f g : P1 →ᵃ[k] P1) : ⇑(f * g) = f ∘ g := rfl
 @[simp] lemma coe_one : ⇑(1 : P1 →ᵃ[k] P1) = _root_.id := rfl
 
+/-- `affine_map.linear` on endomorphisms is a `monoid_hom`. -/
+@[simps] def linear_hom : (P1 →ᵃ[k] P1) →* (V1 →ₗ[k] V1) :=
+{ to_fun := linear,
+  map_one' := rfl,
+  map_mul' := λ _ _, rfl }
+
 include V2
 
 @[simp] lemma injective_iff_linear_injective (f : P1 →ᵃ[k] P2) :