[Merged by Bors] - feat: tensor algebra of free module over integral domain is a domain

Mathlib/Algebra/FreeAlgebra.lean

@@ -5,7 +5,7 @@ Authors: Scott Morrison, Adam Topaz, Eric Wieser
 -/
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
 import Mathlib.Algebra.Algebra.Tower
-import Mathlib.Algebra.MonoidAlgebra.Basic
+import Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
 import Mathlib.RingTheory.Adjoin.Basic
 
 #align_import algebra.free_algebra from "leanprover-community/mathlib"@"6623e6af705e97002a9054c1c05a980180276fc1"
@@ -474,6 +474,12 @@ noncomputable def equivMonoidAlgebraFreeMonoid :
 instance [Nontrivial R] : Nontrivial (FreeAlgebra R X) :=
   equivMonoidAlgebraFreeMonoid.surjective.nontrivial
 
+instance instNoZeroDivisors [NoZeroDivisors R] : NoZeroDivisors (FreeAlgebra R X) :=
+  equivMonoidAlgebraFreeMonoid.toMulEquiv.noZeroDivisors
+
+instance instIsDomain {R X} [CommRing R] [IsDomain R] : IsDomain (FreeAlgebra R X) :=
+  NoZeroDivisors.to_isDomain _
+
 section
 
 /-- The left-inverse of `algebraMap`. -/

Mathlib/Algebra/Group/UniqueProds.lean

@@ -622,3 +622,45 @@ instance {ι G} [AddZeroClass G] [TwoUniqueSums G] : TwoUniqueSums (ι →₀ G)
   `TwoUniqueSums` because it's ordered. -/
 instance [AddCommGroup G] [Module ℚ G] : TwoUniqueSums G :=
   TwoUniqueSums.addHom_image_of_injective _ (Basis.ofVectorSpace ℚ G).repr.injective inferInstance
+
+/-- Any `FreeMonoid` has the `TwoUniqueProds` property. -/
+@[to_additive "Any `FreeAddMonoid` has the `TwoUniqueSums` property."]
+instance FreeMonoid.instTwoUniqueProds {κ : Type*} : TwoUniqueProds (FreeMonoid κ) where
+  uniqueMul_of_one_lt_card {A} {B} h := by
+    have max_length {s : Finset (FreeMonoid κ)} (hs : s.Nonempty) :
+        ∃ w ∈ s, ∀ u ∈ s, u.length ≤ w.length :=
+      have ⟨w, hws, hw⟩ := Finset.mem_image.1 <| (s.image (·.length)).max'_mem (hs.image _)
+      ⟨w, hws, fun u hu => hw ▸ Finset.le_max' _ _ (Finset.mem_image.2 ⟨_, hu, rfl⟩)⟩
+    have min_length {s : Finset (FreeMonoid κ)} (hs : s.Nonempty) :
+        ∃ w ∈ s, ∀ u ∈ s, w.length ≤ u.length :=
+      have ⟨w, hws, hw⟩ := Finset.mem_image.1 <| (s.image (·.length)).min'_mem (hs.image _)
+      ⟨w, hws, fun u hu => hw ▸ Finset.min'_le _ _ (Finset.mem_image.2 ⟨_, hu, rfl⟩)⟩
+    have ⟨hA, hB, hAB⟩ := Nat.one_lt_mul_iff.mp h
+    rw [Finset.card_pos] at hA hB
+    have ⟨x, hxA, hx⟩ := max_length hA
+    have ⟨y, hyB, hy⟩ := max_length hB
+    have ⟨x', hx'A, hx'⟩ := min_length hA
+    have ⟨y', hy'B, hy'⟩ := min_length hB
+    by_cases heq : (x, y) = (x', y')
+    · rw [Finset.one_lt_card, Finset.one_lt_card] at hAB
+      obtain (⟨u, hu, v, hv, hne⟩ | ⟨u, hu, v, hv, hne⟩) := hAB
+      · have hl (u) (hu) := le_antisymm (hx u hu) (congrArg (·.1.length) heq ▸ hx' u hu)
+        exact ⟨(u, y), Finset.mk_mem_product hu hyB, (v, y), Finset.mk_mem_product hv hyB,
+          fun heq => hne (congrArg Prod.fst heq),
+          fun w z hw _ h => List.append_inj h <| (hl w hw).trans (hl u hu).symm,
+          fun w z hw _ h => List.append_inj h <| (hl w hw).trans (hl v hv).symm⟩
+      · have hl (u) (hu) := le_antisymm (hy u hu) (congrArg (·.2.length) heq ▸ hy' u hu)
+        exact ⟨(x, u), Finset.mk_mem_product hxA hu, (x, v), Finset.mk_mem_product hxA hv,
+          fun heq => hne (congrArg Prod.snd heq),
+          fun w z _ hz h => List.append_inj' h <| (hl z hz).trans (hl u hu).symm,
+          fun w z _ hz h => List.append_inj' h <| (hl z hz).trans (hl v hv).symm⟩
+    refine ⟨(x, y), Finset.mk_mem_product hxA hyB, (x', y'), Finset.mk_mem_product hx'A hy'B,
+        heq, fun u v hu hv h => ?_, fun u v hu hv h => ?_⟩
+    · exact List.append_inj h <| And.left <| by
+        rw [← add_eq_add_iff_eq_and_eq (hx u hu) (hy v hv),
+          ← List.length_append, ← List.length_append]
+        exact congrArg List.length h
+    · exact List.append_inj h <| And.left <| by
+        rw [eq_comm, ← add_eq_add_iff_eq_and_eq (hx' u hu) (hy' v hv), eq_comm,
+          ← List.length_append, ← List.length_append]
+        exact congrArg List.length h

Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean

@@ -243,6 +243,10 @@ theorem algebraMap_eq_one_iff (x : R) : algebraMap R (TensorAlgebra R M) x = 1 
   map_eq_one_iff (algebraMap _ _) (algebraMap_leftInverse _).injective
 #align tensor_algebra.algebra_map_eq_one_iff TensorAlgebra.algebraMap_eq_one_iff
 
+/-- A `TensorAlgebra` over a nontrivial semiring is nontrivial. -/
+instance [Nontrivial R] : Nontrivial (TensorAlgebra R M) :=
+  (algebraMap_leftInverse M).injective.nontrivial
+
 variable {M}
 
 /-- The canonical map from `TensorAlgebra R M` into `TrivSqZeroExt R M` that sends

Mathlib/LinearAlgebra/TensorAlgebra/Basis.lean

@@ -63,11 +63,19 @@ instance instModuleFree [Module.Free R M] : Module.Free R (TensorAlgebra R M) :=
   let ⟨⟨_κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
   .of_basis b.tensorAlgebra
 
+instance instNoZeroDivisors [NoZeroDivisors R] [Module.Free R M] :
+    NoZeroDivisors (TensorAlgebra R M) :=
+  have ⟨⟨κ, b⟩⟩ := ‹Module.Free R M›
+  (equivFreeAlgebra b).toMulEquiv.noZeroDivisors
+
 end CommSemiring
 
 section CommRing
 variable [CommRing R] [AddCommGroup M] [Module R M]
 
+instance instIsDomain [IsDomain R] [Module.Free R M] : IsDomain (TensorAlgebra R M) :=
+  NoZeroDivisors.to_isDomain _
+
 attribute [pp_with_univ] Cardinal.lift
 
 open Cardinal in