Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(algebra/monoid_algebra): Add an equivalence between add_monoid_algebra and monoid_algebra in terms of multiplicative #4402

Closed
eric-wieser wants to merge 6 commits into from
Closed

[Merged by Bors] - feat(algebra/monoid_algebra): Add an equivalence between add_monoid_algebra and monoid_algebra in terms of multiplicative #4402

Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
5500504
feat(algebra/monoid_algebra): Add an equivalence between `add_monoid_…
eric-wieser Oct 3, 2020
1ad73f0
chore(*): Corrections thanks to Kevin Buzzard
eric-wieser Oct 14, 2020
f0cc24c
Merge branch 'master' into eric-wieser/monoid_algebra-equiv
eric-wieser Oct 16, 2020
ee17c59
Apply suggestions from code review
eric-wieser Oct 20, 2020
10d9b11
golf
jcommelin Oct 23, 2020
e026b21
chore(*): Simplify using the golfing trick
eric-wieser Oct 23, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 60 additions & 0 deletions src/algebra/monoid_algebra.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -197,6 +197,23 @@ subset.trans support_sum $ bind_mono $ assume a₁ _,

section

/-- Like `finsupp.map_domain_add`, but for the convolutive multiplication we define in this file -/
lemma map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*} [semiring β] [monoid α] [monoid α₂]
{x y : monoid_algebra β α} (f : mul_hom α α₂) :
(map_domain f (x * y : monoid_algebra β α) : monoid_algebra β α₂) =
(map_domain f x * map_domain f y : monoid_algebra β α₂) :=
begin
simp_rw [mul_def, map_domain_sum, map_domain_single, f.map_mul],
rw finsupp.sum_map_domain_index,
{ congr,
ext a b,
rw finsupp.sum_map_domain_index,
{ simp },
{ simp [mul_add] } },
{ simp },
{ simp [add_mul] }
end

variables (k G)

/-- Embedding of a monoid into its monoid algebra. -/
Expand Down Expand Up @@ -620,6 +637,24 @@ lemma single_mul_single {a₁ a₂ : G} {b₁ b₂ : k} :
(sum_single_index (by simp only [zero_mul, single_zero, sum_zero])).trans
(sum_single_index (by rw [mul_zero, single_zero]))

/-- Like `finsupp.map_domain_add`, but for the convolutive multiplication we define in this file -/
lemma map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*}
[semiring β] [add_monoid α] [add_monoid α₂]
{x y : add_monoid_algebra β α} (f : add_hom α α₂) :
(map_domain f (x * y : add_monoid_algebra β α) : add_monoid_algebra β α₂) =
(map_domain f x * map_domain f y : add_monoid_algebra β α₂) :=
begin
simp_rw [mul_def, map_domain_sum, map_domain_single, f.map_add],
rw finsupp.sum_map_domain_index,
{ congr,
ext a b,
rw finsupp.sum_map_domain_index,
{ simp },
{ simp [mul_add] } },
{ simp },
{ simp [add_mul] }
end

section

variables (k G)
Expand Down Expand Up @@ -667,6 +702,31 @@ f.single_mul_apply_aux r _ _ _ $ λ a, by rw [zero_add]

end misc_theorems

end add_monoid_algebra

/-!
#### Conversions between `add_monoid_algebra` and `monoid_algebra`

While we were not able to define `add_monoid_algebra k G = monoid_algebra k (multiplicative G)` due
to definitional inconveniences, we can still show the types are isomorphic.
-/

/-- The equivalence between `add_monoid_algebra` and `monoid_algebra` in terms of `multiplicative` -/
protected def add_monoid_algebra.to_multiplicative [semiring k] [add_monoid G] :
add_monoid_algebra k G ≃+* monoid_algebra k (multiplicative G) :=
{ map_mul' := λ x y, by convert add_monoid_algebra.map_domain_mul (add_hom.id G),
..finsupp.dom_congr multiplicative.of_add }

/-- The equivalence between `monoid_algebra` and `add_monoid_algebra` in terms of `additive` -/
protected def monoid_algebra.to_additive [semiring k] [monoid G] :
monoid_algebra k G ≃+* add_monoid_algebra k (additive G) :=
{ map_mul' := λ x y, by convert monoid_algebra.map_domain_mul (mul_hom.id G),
..finsupp.dom_congr additive.of_mul }
Copy link
Member

@kbuzzard kbuzzard Oct 13, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Aah! If you make multiplicative irreducible, we see that this line is also abusing type equality.

type mismatch at field 'to_fun'
  (finsupp.dom_congr multiplicative.to_add).to_fun
has type
  (multiplicative ?m_1 →₀ ?m_2) → ?m_1 →₀ ?m_2 : Type (max ? ?)
but is expected to have type
  add_monoid_algebra k G → monoid_algebra k (multiplicative G) : Type (max (max u₂ u₁) u₁ u₂)

This is the problem -- multiplicative is on the wrong side.

Copy link
Member

@kbuzzard kbuzzard Oct 13, 2020 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more. 

protected def add_monoid_algebra.of_multiplicative [semiring k] [add_monoid G] :
  monoid_algebra k (multiplicative G) ≃+* add_monoid_algebra k G :=
{ map_mul' := λ x y, by {
    simp only [finsupp.dom_congr],
    sorry
  },
  ..finsupp.dom_congr multiplicative.to_add }

This typechecks even if multiplicative is irreducible. Note that I switched the order of the equiv! (and hence changed the name).

But now you need a result which applies to to_add so it can't have the hypotheses of your f in the mul' lemma.

Copy link
Member

@kbuzzard kbuzzard Oct 13, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BTW making multiplicative irreducible shows that there is also type abuse going on in lift (which is already in mathlib) -- for example

type mismatch at application
  ⇑F a
term
  a
has type
  G
but is expected to have type
  multiplicative G

error in definition of lift.to_fun. Type abuse like this creates problems down the line (e.g. the earlier problem about p*q=p+q) and I've found that making stuff like multiplicative irreducible stops this sort of thing happening.

Copy link
Member Author

@eric-wieser eric-wieser Oct 14, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the problem -- multiplicative is on the wrong side.

Thanks for catching this - but this was a mistake in just one of the two definitions.

Copy link
Member Author

@eric-wieser eric-wieser Oct 14, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is a case of two wrong make a right. After the simp only [finsupp.dom_congr], line, the goal is:

--                                 VVVVV add_monoid_algebra k G
map_domain ⇑multiplicative.of_add (x * y) =
-- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ monoid_algebra k multiplicative(G)
  map_domain ⇑multiplicative.of_add x * map_domain ⇑multiplicative.of_add y

map_domain doesn't know about *_monoid_algebra, so has signature (G →₀ k) → (multiplicative G →₀ k). At this point, we've done our first sneaky step in type abuse - we're considering the input an add_monoid_algebra, and the output a monoid_algebra - even though map_domain_mul' implies that both input and output are of the same type.

The second wrong is the tricks we already see in (f).

This would all be a lot easier if we could do away with add_*, and have monoid_algebra k G (+) and monoid_algebra k G (*) as our two versions...

Copy link
Member

@kbuzzard kbuzzard Oct 20, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that sneaky steps in type abuse should be avoided if at all possible. Can't we also use to_add and of_add etc to work around this?

Copy link
Member Author

@eric-wieser eric-wieser Oct 20, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd argue that type abuse is only a problem in definitions. In proofs, it shouldn't matter - as long as the theorem statement plays no tricks, then proof irrelevance means that abuse in the proof doesn't matter, right?

Copy link
Member Author

@eric-wieser eric-wieser Oct 20, 2020 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Now, I could replace the proof

apply monoid_algebra.map_domain_mul',
intros p q,
simp only [of_mul_mul],
refl

with

    simp only [finsupp.dom_congr],
    rw monoid_algebra.mul_def,
    rw add_monoid_algebra.mul_def,
    simp_rw [map_domain_sum, map_domain_single, of_mul_mul],
    rw finsupp.sum_map_domain_index,
    { congr,
      ext a b,
      rw finsupp.sum_map_domain_index,
      { simp },
      { simp [mul_add] } },
    { simp },
    { simp [add_mul] },

but that amounts to a copy-paste of monoid_algebra.map_domain_mul, with:

  • One monoid_algebra.mul_def replaced with add_monoid_algebra.mul_def
  • f.map_mul replaced with of_mul_mul

Given the whole point of the multiplicative type tag is to avoid duplicate lemmas, is this really worth it?


namespace add_monoid_algebra

variables {k G}

/-! #### Algebra structure -/
section algebra

Expand Down