# Zulip Chat Archive

## Stream: general

### Topic: type synonym instances

#### Jireh Loreaux (Mar 11 2022 at 17:22):

I am trying to define the (minimal) unitization of a non-unital`R`

-algebra as a type synonym for `R × A`

. But I can't seem to get Lean to disregard the `prod.has_mul`

instance. What am I doing wrong here? (Note: the `simp`

shows that Lean is using the wrong multiplication).

```
import algebra.algebra.basic
def algebra.unitization (R A : Type*) [comm_ring R] [non_unital_ring A] := R × A
variables {R A : Type*} [comm_ring R] [non_unital_ring A]
open algebra
local attribute [-instance] prod.has_mul prod.has_one
instance : add_comm_group (unitization R A) := prod.add_comm_group
instance [module R A] : module R (unitization R A) := prod.module
instance : has_one (unitization R A) := { one := (1, 0) }
instance [module R A] : has_mul (unitization R A) :=
{ mul := λ ⟨r₁, a₁⟩ ⟨r₂, a₂⟩, (r₁ * r₂, r₁ • a₂ + r₂ • a₁ + a₁ * a₂) }
@[simp]
lemma one_def : (1 : unitization R A) = (1, 0) := rfl
@[simp]
lemma mul_def [module R A] (r₁ r₂ : R) (a₁ a₂ : A) :
((r₁, a₁) : unitization R A) * (r₂, a₂) = (r₁ * r₂, r₁ • a₂ + r₂ • a₁ + a₁ * a₂) :=
begin
simp,
-- ⊢ r₁ • a₂ + r₂ • a₁ = 0
sorry
end
```

#### Eric Rodriguez (Mar 11 2022 at 17:27):

firstly, the first issue is that Lean elaborates the mul as a mul of the `prod`

type anyways, if you look at the widget

#### Yaël Dillies (Mar 11 2022 at 17:28):

You might want to try making `unitization`

irreducible.

#### Jireh Loreaux (Mar 11 2022 at 17:30):

Why does it elaborate it as the `prod`

version if I removed that instance? I thought I would probably make unitization irreducible at the end, when I'm done with everything I need. Is that the wrong approach?

#### Yaël Dillies (Mar 11 2022 at 17:30):

You should use "identity" equivalences to explicitly mark the conversions

```
import algebra.algebra.basic
def algebra.unitization (R A : Type*) [comm_ring R] [non_unital_ring A] := R × A
variables {R A : Type*} [comm_ring R] [non_unital_ring A]
open algebra
def to_unitization : R × A ≃ unitization R A := equiv.refl _
def of_unitization : unitization R A ≃ R × A := equiv.refl _
local attribute [-instance] prod.has_mul prod.has_one
instance : add_comm_group (unitization R A) := prod.add_comm_group
instance [module R A] : module R (unitization R A) := prod.module
instance : has_one (unitization R A) := { one := (1, 0) }
instance [module R A] : has_mul (unitization R A) :=
{ mul := λ ⟨r₁, a₁⟩ ⟨r₂, a₂⟩, (r₁ * r₂, r₁ • a₂ + r₂ • a₁ + a₁ * a₂) }
@[simp]
lemma mul_def [module R A] (r₁ r₂ : R) (a₁ a₂ : A) :
to_unitization (r₁, a₁) * to_unitization (r₂, a₂) = (r₁ * r₂, r₁ • a₂ + r₂ • a₁ + a₁ * a₂) :=
sorry
```

#### Eric Rodriguez (Mar 11 2022 at 17:30):

sorry, not just the `mul`

, but like each individual element

#### Eric Rodriguez (Mar 11 2022 at 17:31):

I'm unsure why Lean does this but maybe if you set the expected type on the right, it will work out anyways (I _think_ Lean elaborates right to left, not sure)

#### Eric Rodriguez (Mar 11 2022 at 17:32):

wow, not even `((r₁, a₁) : unitization R A) * ((r₂, a₂): unitization R A) = ((r₁ * r₂, r₁ • a₂ + r₂ • a₁ + a₁ * a₂) : unitization R A)`

works.

#### Jireh Loreaux (Mar 11 2022 at 17:32):

I tried before giving explicit types to all of them and it still had the same problem, but I'll use the identity equivalences.

#### Jireh Loreaux (Mar 11 2022 at 17:32):

yeah, that's why I was so confused.

#### Eric Rodriguez (Mar 11 2022 at 17:33):

`((r₁, a₁) * (r₂, a₂): unitization R A) = (r₁ * r₂, r₁ • a₂ + r₂ • a₁ + a₁ * a₂)`

also works, but yikes

#### Jireh Loreaux (Mar 11 2022 at 17:33):

But still, why doesn't `local attribute [-instance] prod.has_mul`

help at all?

#### Eric Rodriguez (Mar 11 2022 at 17:34):

because there's `prod.distrib`

, `prod.semiring`

, `prod.non_assoc_semiring`

.... and they all imply the `has_mul`

instance

#### Kevin Buzzard (Mar 11 2022 at 17:34):

This is probably unrelated, but generally people say "don't make definitions using `λ ⟨r₁, a₁⟩ ⟨r₂, a₂⟩, ...`

, instead use `{ mul := λ ra₁ ra₂, (ra₁.1 * ra₂.1, ra₁.1 • ra₂.2 + ra₂.1 • ra₁.2 + ra₁.2 * ra₂.2) }`

"

#### Eric Rodriguez (Mar 11 2022 at 17:34):

you can also see this on the widgeet: image.png

#### Jireh Loreaux (Mar 11 2022 at 17:36):

I've never clicked on the highlight-on-hover in the widget panel :face_palm: Can't believe I've been missing this.

#### Kevin Buzzard (Mar 11 2022 at 17:38):

The reason it's using the wrong product is a pretty common gotcha: `((r₁, a₁) : unitization R A)`

does *not* mean "make `(r₁, a₁)`

have type `unitization R A`

", it means "check that its type is defeq to `unitization R A`

but don't actually change the type unless you need to solve a unification problem"

#### Kevin Buzzard (Mar 11 2022 at 17:40):

The reason the `(id (r₁, a₁) : unitization R A)`

trick works (this is a cheap fix by the way) is that this type checking sanity thing occurs before Lean decides which `\alpha`

it's going to use in `@id \alpha x y`

, so Lean is persuaded to let alpha be `unitization R A`

.

#### Jireh Loreaux (Mar 11 2022 at 17:47):

What's the reasoning behind "don't make definitions using `λ ⟨r₁, a₁⟩ ⟨r₂, a₂⟩, ...,`

" ? Is it some kind of normal form issue?

#### Eric Rodriguez (Mar 11 2022 at 17:48):

try `#print`

the definition

#### Kevin Buzzard (Mar 11 2022 at 17:54):

Mmm, `._match_2`

. The approach I suggested unfolds much better.

#### Eric Rodriguez (Mar 11 2022 at 17:57):

(although I will say that whenever I've done it `simp!`

has dealt with this sort of stuff super well)

#### Johan Commelin (Mar 11 2022 at 18:03):

@Jireh Loreaux If you apply it to something of the form `x + 3*y`

, then Lean doesn't know how to turn that into `⟨r₁, a₁⟩`

automatically. So the definition will not unfold. But it doesn't have problems with `(x + 3*y).1`

and `(x + 3*y).2`

.

The reason is that `foo : X × Y`

is not defeq to `⟨foo.1, foo.2⟩`

in Lean 3. (I think in Lean 4 this problem is gone.)

Last updated: Aug 03 2023 at 10:10 UTC