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

[bustercopley]

Provide instances

• Nontrivial (TensorAlgebra R M) when M is a module over
  a nontrivial semiring R
• NoZeroDivisors (FreeAlgebra R X) when R is a commutative
  semiring with no zero-divisors and X any type
• IsDomain (FreeAlgebra R X) when R is an integral domain
  and X is any type
• TwoUniqueProds (FreeMonoid X) where X is any type
  (this provides NoZeroDivisors (MonoidAlgebra R (FreeMonoid X))
  when R is a semiring and X any type,
  via TwoUniqueProds.toUniqueProds
  and MonoidAlgebra.instNoZeroDivisorsOfUniqueProds)
• NoZeroDivisors (TensorAlgebra R M) when M is a free module
  over a commutative semiring R with no zero-divisors
• IsDomain (TensorAlgebra R M) when M is a free module over
  an integral domain R

In Algebra.Group.UniqueProds:

• Rename UniqueProds.mulHom_image_of_injective to
  UniqueProds.of_injective_mulHom.
• New lemmas UniqueMul.of_mulHom_image, UniqueProds.of_mulHom,
  TwoUniqueProds.of_mulHom show the relevant property holds in the
  domain of a multiplicative homomorphism if it holds in the codomain,
  under a certain hypothesis on the homomorphism.

[eric-wieser]

LGTM! I'll maybe give @adomani time to come give this a final look before merging

(and of course, you should look at it when it's not super late in case you had any more ideas)

[adomani]

This is all very nice, thanks!

I wonder whether this result should be more "generic" in terms of (Two)UniqueProds for Lists, Multisets, Finsets, as TwoUniqueProds.instTwoUniqueProdsProdInstMul works for products.

In fact, using a Lex order on Lists and an arbitrary linear order on the underlying type X should give an argument very similar to the one for the MVPolynomials result.

[eric-wieser]

I wonder whether this result should be more "generic" in terms of (Two)UniqueProds for Lists, Multisets, Finsets, as TwoUniqueProds.instTwoUniqueProdsProdInstMul works for products.

This should indeed work for TwoUniqueSums and Multiset, but none of the other types have an Add or Mul with the right semantics, so I don't think this can work there.

[adomani]

This should indeed work for TwoUniqueSums and Multiset, but none of the other types have an Add or Mul with the right semantics, so I don't think this can work there.

Ah, I see! What about exploiting a little of TwoUniqueSums.of_covariant_left, since FreeMonoid is cancellative?

[eric-wieser]

I tried that, but it needs a linear order. Indeed, there should be some common result that both the instance in this PR and the one you refer to can be constructed from.

[adomani]

I'll try this when I have some more time. What I had in mind was to use a lex ordering on Lists and any linear order on the base type X, i.e. one that you obtain via a LinearExtension.

In the multiset case, I think that you are also extracting both the min and the max for a lex order on any linear extension. Anyway, I may have some time to try this out tonight or tomorrow, but this is just a way of golfing further the PR: I am happy with the results, even if I think that the proofs can be streamlined.

[bustercopley]

Reviewers, thank you very much for your work on this. It's been an education.

Do you have any further suggestions?

• Do you think "grade" is ok? Can you see a better phrasing?
• More docstrings? [edit: done]

[bustercopley]

No more improvements have come to mind. @eric-wieser, any suggestions? Do you think this should be merged, and do you think it's ready? Anything else I should do (like ask another person to review)?

[alreadydone]

@adomani Do you remember why you called this lemma mulHom_image_of_injective in #6723? I can't see image in the statement (but the proof uses mulHom_image_iff) and I think of_injective_mulHom might be a better name.

theorem mulHom_image_of_injective (f : H →ₙ* G) (hf : Function.Injective f) (uG : UniqueProds G) :
    UniqueProds H 

[alreadydone]

I've completed a refactor that cuts 18 lines off the PR and proves the more general

@[to_additive] theorem of_mulHom (f : H →ₙ* G)
    (hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d)
    (uG : TwoUniqueProds G) : TwoUniqueProds H where

Feel free to merge!

[bustercopley]

Merged. of_mulHom is great!

[adomani]

@adomani Do you remember why you called this lemma mulHom_image_of_injective in #6723? I can't see image in the statement (but the proof uses mulHom_image_iff) and I think of_injective_mulHom might be a better name.

theorem mulHom_image_of_injective (f : H →ₙ* G) (hf : Function.Injective f) (uG : UniqueProds G) :
    UniqueProds H 

I think that your name is indeed better. I suspect that the name that I gave referred to an older version of the lemma that might have contained an image...

[alreadydone]

Thanks! I wouldn't have thought of the condition hf without you extracting of_graded_mul; my hf is simply a weakened form of your hinj that assumes f b = f d in addition. What I observed is that in

theorem of_graded_mul {X G : Type*} [Mul X] [Add G] [IsRightCancelAdd G] [LinearOrder G]
    [CovariantClass G G (· + ·) (· < ·)] [CovariantClass G G (Function.swap (· + ·)) (· < ·)]
    {f : X → G} (hf : ∀ x y : X, f (x * y) = f x + f y)
    (hinj : ∀ a b c d : X, a * b = c * d → f a = f c → a = c ∧ b = d) :
    TwoUniqueProds X where

(let's pretend everything is multiplicative) hf is saying that f is a MulHom, and the conditions on G guarantees that G has TwoUniqueProds by TwoUniqueProds.of_covariant_right. Once I realized these it's natural to come up with of_mulHom.
This PR looks good to me now, but I just noticed no one ever added any labels to it? I added two and I'll wait a day for comments before sending it to maintainers.

[alreadydone]

Since we renamed mulHom_image_of_injective, I've now also renamed mulHom_image_iff for consistency.

[alreadydone]

And added deprecated aliases. (I doubt anyone is using them, but still ...)

[alreadydone]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by alreadydone.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style