type synonym instances

Stream: general

[Jireh Loreaux]

I am trying to define the (minimal) unitization of a non-unitalR-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]

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]

You might want to try making unitization irreducible.

[Jireh Loreaux]

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]

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]

sorry, not just the mul, but like each individual element

[Eric Rodriguez]

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]

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]

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]

yeah, that's why I was so confused.

[Eric Rodriguez]

((r₁, a₁) * (r₂, a₂): unitization R A) = (r₁ * r₂, r₁ • a₂ + r₂ • a₁ + a₁ * a₂) also works, but yikes

[Jireh Loreaux]

But still, why doesn't local attribute [-instance] prod.has_mul help at all?

[Eric Rodriguez]

because there's prod.distrib, prod.semiring, prod.non_assoc_semiring.... and they all imply the has_mul instance

[Kevin Buzzard]

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]

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

[Jireh Loreaux]

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]

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]

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]

What's the reasoning behind "don't make definitions using λ ⟨r₁, a₁⟩ ⟨r₂, a₂⟩, ...," ? Is it some kind of normal form issue?

[Eric Rodriguez]

try #print the definition

[Kevin Buzzard]

Mmm, ._match_2. The approach I suggested unfolds much better.

[Eric Rodriguez]

(although I will say that whenever I've done it simp! has dealt with this sort of stuff super well)

[Johan Commelin]

@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.)