feat(algebra/invertible): map_inv_of and some other basic results (#…

…16202)

The titular lemma states that under suitable conditions, `f (⅟r) = ⅟(f r)`.

This also provides some lemmas about left inverses, which are motivated primarily by proving `is_unit (algebra_map R (exterior_algebra R M) r) ↔ is_unit r`.

src/algebra/hom/units.lean

@@ -125,14 +125,25 @@ units.lift_right f
 end monoid_hom
 
 namespace is_unit
-variables {F α M N : Type*}
+variables {F G α M N : Type*}
 
 section monoid
 variables [monoid M] [monoid N]
 
 @[to_additive] lemma map [monoid_hom_class F M N] (f : F) {x : M} (h : is_unit x) : is_unit (f x) :=
 by rcases h with ⟨y, rfl⟩; exact (units.map (f : M →* N) y).is_unit
 
+@[to_additive] lemma of_left_inverse [monoid_hom_class F M N] [monoid_hom_class G N M]
+  {f : F} {x : M} (g : G) (hfg : function.left_inverse g f) (h : is_unit (f x)) :
+  is_unit x :=
+by simpa only [hfg x] using h.map g
+
+@[to_additive] lemma _root_.is_unit_map_of_left_inverse
+  [monoid_hom_class F M N] [monoid_hom_class G N M]
+  {f : F} {x : M} (g : G) (hfg : function.left_inverse g f) :
+  is_unit (f x) ↔ is_unit x :=
+⟨of_left_inverse g hfg, map _⟩
+
 /-- If a homomorphism `f : M →* N` sends each element to an `is_unit`, then it can be lifted
 to `f : M →* Nˣ`. See also `units.lift_right` for a computable version. -/
 @[to_additive "If a homomorphism `f : M →+ N` sends each element to an `is_add_unit`, then it can be

src/algebra/invertible.lean

@@ -107,7 +107,8 @@ instance [monoid α] (a : α) : subsingleton (invertible a) :=
 ⟨ λ ⟨b, hba, hab⟩ ⟨c, hca, hac⟩, by { congr, exact left_inv_eq_right_inv hba hac } ⟩
 
 /-- If `r` is invertible and `s = r`, then `s` is invertible. -/
-def invertible.copy [monoid α] {r : α} (hr : invertible r) (s : α) (hs : s = r) : invertible s :=
+def invertible.copy [mul_one_class α] {r : α} (hr : invertible r) (s : α) (hs : s = r) :
+  invertible s :=
 { inv_of := ⅟r,
   inv_of_mul_self := by rw [hs, inv_of_mul_self],
   mul_inv_of_self := by rw [hs, mul_inv_of_self] }
@@ -272,3 +273,31 @@ def invertible.map {R : Type*} {S : Type*} {F : Type*} [mul_one_class R] [mul_on
 { inv_of := f (⅟r),
   inv_of_mul_self := by rw [←map_mul, inv_of_mul_self, map_one],
   mul_inv_of_self := by rw [←map_mul, mul_inv_of_self, map_one] }
+
+/-- Note that the `invertible (f r)` argument can be satisfied by using `letI := invertible.map f r`
+before applying this lemma. -/
+lemma map_inv_of {R : Type*} {S : Type*} {F : Type*} [mul_one_class R] [monoid S]
+  [monoid_hom_class F R S] (f : F) (r : R) [invertible r] [invertible (f r)] :
+  f (⅟r) = ⅟(f r) :=
+by { letI := invertible.map f r, convert rfl }
+
+/-- A monoid hom with a left-inverse that is also a monoid hom is invertible.
+
+The inverse is computed as `g (⅟(f r))` -/
+@[simps {attrs := []}]
+def invertible.of_left_inverse {R : Type*} {S : Type*} {F G : Type*}
+  [mul_one_class R] [mul_one_class S] [monoid_hom_class F R S] [monoid_hom_class G S R]
+  (f : F) (g : G) (r : R) (h : function.left_inverse g f) [invertible (f r)] :
+  invertible r :=
+(invertible.map g (f r)).copy _ (h r).symm
+
+/-- Invertibility on either side of a monoid hom with a left-inverse is equivalent. -/
+@[simps]
+def invertible_equiv_of_left_inverse {R : Type*} {S : Type*} {F G : Type*}
+  [monoid R] [monoid S] [monoid_hom_class F R S] [monoid_hom_class G S R]
+  (f : F) (g : G) (r : R) (h : function.left_inverse g f) :
+  invertible (f r) ≃ invertible r :=
+{ to_fun := λ _, by exactI invertible.of_left_inverse f _ _ h,
+  inv_fun := λ _, by exactI invertible.map f _,
+  left_inv := λ x, subsingleton.elim _ _,
+  right_inv := λ x, subsingleton.elim _ _ }

src/linear_algebra/exterior_algebra/basic.lean

@@ -149,6 +149,15 @@ map_eq_zero_iff (algebra_map _ _) (algebra_map_left_inverse _).injective
 @[simp] lemma algebra_map_eq_one_iff (x : R) : algebra_map R (exterior_algebra R M) x = 1 ↔ x = 1 :=
 map_eq_one_iff (algebra_map _ _) (algebra_map_left_inverse _).injective
 
+lemma is_unit_algebra_map (r : R) : is_unit (algebra_map R (exterior_algebra R M) r) ↔ is_unit r :=
+is_unit_map_of_left_inverse _ (algebra_map_left_inverse M)
+
+/-- Invertibility in the exterior algebra is the same as invertibility of the base ring. -/
+@[simps]
+def invertible_algebra_map_equiv (r : R) :
+  invertible (algebra_map R (exterior_algebra R M) r) ≃ invertible r :=
+invertible_equiv_of_left_inverse _ _ _ (algebra_map_left_inverse M)
+
 variables {M}
 
 /-- The canonical map from `exterior_algebra R M` into `triv_sq_zero_ext R M` that sends