feat(RingTheory): an algebra that is an invertible module is isomorphic to the base ring (leanprover-community#29954)

This PR considers the case where we have an `R`-algebra `A` which is also an invertible `R`-module, then constructs an isomorphism between `R` and `A` as `R`-algebras:
```lean
variable (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] [Module.Invertible R A]
def algEquivOfRing : R ≃ₐ[R] A :=
```

Author: kckennylau

Mathlib/Algebra/Algebra/Equiv.lean

@@ -817,3 +817,25 @@ def ULift.algEquiv {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Alge
     ULift.{w} A ≃ₐ[R] A where
   __ := ULift.ringEquiv
   commutes' _ := rfl
+
+/-- If an `R`-algebra `A` is isomorphic to `R` as `R`-module, then the canonical map `R → A` is an
+equivalence of `R`-algebras.
+
+Note that if `e : R ≃ₗ[R] A` is the linear equivalence, then this is not the same as the equivalence
+of algebras provided here unless `e 1 = 1`. -/
+@[simps] def LinearEquiv.algEquivOfRing
+    {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
+    (e : R ≃ₗ[R] A) : R ≃ₐ[R] A where
+  __ := Algebra.ofId R A
+  invFun x := e.symm (e 1 * x)
+  left_inv x := calc
+    e.symm (e 1 * (algebraMap R A) x)
+      = e.symm (x • e 1) := by rw [Algebra.smul_def, mul_comm]
+    _ = x := by rw [map_smul, e.symm_apply_apply, smul_eq_mul, mul_one]
+  right_inv x := calc
+    (algebraMap R A) (e.symm (e 1 * x))
+      = (algebraMap R A) (e.symm (e 1 * x)) * e (e.symm 1 • 1) := by
+          rw [smul_eq_mul, mul_one, e.apply_symm_apply, mul_one]
+    _ = x := by rw [map_smul, Algebra.smul_def, mul_left_comm, ← Algebra.smul_def _ (e 1),
+          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, ← mul_assoc, ← Algebra.smul_def,
+          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, one_mul]

Mathlib/RingTheory/PicardGroup.lean

@@ -281,12 +281,83 @@ theorem bijective_of_surjective [Module.Invertible R N] {f : M →ₗ[R] N}
   simpa [lTensor_bijective_iff] using bijective_self_of_surjective
     (f.lTensor _ ∘ₗ (linearEquiv R M).symm.toLinearMap) (by simpa [lTensor_surjective_iff] using hf)
 
+section LinearEquiv
+variable {R M N} [Module.Invertible R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M}
+
+theorem rightInverse_of_leftInverse (hfg : Function.LeftInverse f g) :
+    Function.RightInverse f g :=
+  Function.rightInverse_of_injective_of_leftInverse
+    (bijective_of_surjective hfg.surjective).injective hfg
+
+theorem leftInverse_of_rightInverse (hfg : Function.RightInverse f g) :
+    Function.LeftInverse f g :=
+  rightInverse_of_leftInverse hfg
+
+variable (f g) in
+theorem leftInverse_iff_rightInverse :
+    Function.LeftInverse f g ↔ Function.RightInverse f g :=
+  ⟨rightInverse_of_leftInverse, leftInverse_of_rightInverse⟩
+
+/-- If `f : M →ₗ[R] N` and `g : N →ₗ[R] M` where `M` and `N` are invertible `R`-modules, and `f` is
+a left inverse of `g`, then in fact `f` is also the right inverse of `g`, and we promote this to
+an `R`-module isomorphism. -/
+def linearEquivOfLeftInverse (hfg : Function.LeftInverse f g) : M ≃ₗ[R] N :=
+  .ofLinear f g (LinearMap.ext hfg) (LinearMap.ext <| rightInverse_of_leftInverse hfg)
+
+@[simp] lemma linearEquivOfLeftInverse_apply (hfg : Function.LeftInverse f g) (x : M) :
+    linearEquivOfLeftInverse hfg x = f x := rfl
+
+@[simp] lemma linearEquivOfLeftInverse_symm_apply (hfg : Function.LeftInverse f g) (x : N) :
+    (linearEquivOfLeftInverse hfg).symm x = g x := rfl
+
+/-- If `f : M →ₗ[R] N` and `g : N →ₗ[R] M` where `M` and `N` are invertible `R`-modules, and `f` is
+a right inverse of `g`, then in fact `f` is also the left inverse of `g`, and we promote this to
+an `R`-module isomorphism. -/
+def linearEquivOfRightInverse (hfg : Function.RightInverse f g) : M ≃ₗ[R] N :=
+  .ofLinear f g (LinearMap.ext <| leftInverse_of_rightInverse hfg) (LinearMap.ext hfg)
+
+@[simp] lemma linearEquivOfRightInverse_apply (hfg : Function.RightInverse f g) (x : M) :
+    linearEquivOfRightInverse hfg x = f x := rfl
+
+@[simp] lemma linearEquivOfRightInverse_symm_apply (hfg : Function.RightInverse f g) (x : N) :
+    (linearEquivOfRightInverse hfg).symm x = g x := rfl
+
+end LinearEquiv
+
 section Algebra
 
+section algEquivOfRing
+variable (A : Type*) [Semiring A] [Algebra R A] [Module.Invertible R A]
+
+/-- If an `R`-algebra `A` is also an invertible `R`-module, then it is in fact isomorphic to the
+base ring `R`. The algebra structure gives us a map `A ⊗ A → A`, which after tensoring by `Aᵛ`
+becomes a map `A → R`, which is the inverse map we seek. -/
+noncomputable def algEquivOfRing : R ≃ₐ[R] A :=
+  let inv : A →ₗ[R] R :=
+    linearEquiv R A ∘ₗ
+      (LinearMap.mul' R A).lTensor (Dual R A) ∘ₗ
+      (leftCancelEquiv A (linearEquiv R A)).symm
+  have right : inv ∘ₗ Algebra.linearMap R A = LinearMap.id :=
+    let ⟨s, hs⟩ := exists_finset ((linearEquiv R A).symm 1)
+    LinearMap.ext_ring <| by simp [inv, hs, sum_tmul, map_sum, ← (LinearEquiv.symm_apply_eq _).1 hs]
+  { linearEquivOfRightInverse (f := Algebra.linearMap R A) (g := inv) (LinearMap.ext_iff.1 right),
+    Algebra.ofId R A with }
+
+variable {A} in
+@[simp] lemma algEquivOfRing_apply (x : R) : algEquivOfRing R A x = algebraMap R A x := rfl
+
+end algEquivOfRing
+
 instance : Module.Invertible A (A ⊗[R] M) :=
   .right (M := A ⊗[R] Dual R M) <| (AlgebraTensorModule.distribBaseChange ..).symm ≪≫ₗ
     AlgebraTensorModule.congr (.refl A A) (linearEquiv R M) ≪≫ₗ AlgebraTensorModule.rid ..
 
+variable {R M N A} in
+theorem of_isLocalization (S : Submonoid R) [IsLocalization S A]
+    (f : M →ₗ[R] N) [IsLocalizedModule S f] [Module A N] [IsScalarTower R A N] :
+    Module.Invertible A N :=
+  .congr (IsLocalizedModule.isBaseChange S A f).equiv
+
 instance (L) [AddCommMonoid L] [Module R L] [Module A L] [IsScalarTower R A L]
     [Module.Invertible A L] : Module.Invertible A (L ⊗[R] M) :=
   .congr (AlgebraTensorModule.cancelBaseChange R A A L M)