chore: drop Algebra.TensorProduct.rightAlgebra' (#184)

ImperialCollegeLondon · Oct 31, 2024 · 723052b · 723052b
1 parent 94b750a
commit 723052b
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 20 deletions.
diff --git a/FLT/AutomorphicForm/QuaternionAlgebra.lean b/FLT/AutomorphicForm/QuaternionAlgebra.lean
@@ -33,7 +33,7 @@ noncomputable abbrev incl₁ : Dˣ →* Dfx F D :=
   Units.map Algebra.TensorProduct.includeLeftRingHom.toMonoidHom
 
 noncomputable abbrev incl₂ : (FiniteAdeleRing (𝓞 F) F)ˣ →* Dfx F D :=
-  Units.map Algebra.TensorProduct.rightAlgebra'.toMonoidHom
+  Units.map Algebra.TensorProduct.rightAlgebra.toMonoidHom
 
 /-!
 This definition is made in mathlib-generality but is *not* the definition of an automorphic

diff --git a/FLT/DivisionAlgebra/Finiteness.lean b/FLT/DivisionAlgebra/Finiteness.lean
@@ -33,32 +33,16 @@ section missing_instances
 
 variable {R D A : Type*} [CommSemiring R] [Semiring D] [CommSemiring A] [Algebra R D] [Algebra R A]
 
--- Algebra.TensorProduct.rightAlgebra has unnecessary commutativity assumptions
--- This should be fixed in mathlib; ideally it should be an exact mirror of leftAlgebra but
--- I ignore S as I don't need it.
-def Algebra.TensorProduct.rightAlgebra' : Algebra A (D ⊗[R] A) :=
-  Algebra.TensorProduct.includeRight.toRingHom.toAlgebra' (by
-    simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.includeRight_apply]
-    intro a b
-    apply TensorProduct.induction_on (motive := fun b ↦ 1 ⊗ₜ[R] a * b = b * 1 ⊗ₜ[R] a)
-    · simp only [mul_zero, zero_mul]
-    · intro d a'
-      simp only [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_one,
-        NonUnitalCommSemiring.mul_comm]
-    · intro x y hx hy
-      rw [left_distrib, hx, hy, right_distrib]
-    )
-
 -- this makes a diamond for Algebra A (A ⊗[R] A) which will never happen here
-attribute [local instance] Algebra.TensorProduct.rightAlgebra'
+attribute [local instance] Algebra.TensorProduct.rightAlgebra
 
 -- These seem to be missing
 instance [Module.Finite R D] : Module.Finite A (D ⊗[R] A) := sorry
 instance [Module.Free R D]  : Module.Free A (D ⊗[R] A) := sorry
 
 end missing_instances
 
-attribute [local instance] Algebra.TensorProduct.rightAlgebra'
+attribute [local instance] Algebra.TensorProduct.rightAlgebra
 
 variable (K : Type*) [Field K] [NumberField K]
 variable (D : Type*) [DivisionRing D] [Algebra K D]
@@ -81,7 +65,7 @@ noncomputable abbrev incl₁ : Dˣ →* Dfx K D :=
   Units.map Algebra.TensorProduct.includeLeftRingHom.toMonoidHom
 
 noncomputable abbrev incl₂ : (FiniteAdeleRing (𝓞 K) K)ˣ →* Dfx K D :=
-  Units.map Algebra.TensorProduct.rightAlgebra'.toMonoidHom
+  Units.map Algebra.TensorProduct.rightAlgebra.toMonoidHom
 
 -- Voight "Main theorem 27.6.14(b) (Fujisaki's lemma)"
 /-!