Free rings

Stream: new members

[Zhangir Azerbayev]

I'm trying to work with free rings, but I'm getting some errors I don't understand related to type class instances.

import tactic
import ring_theory.free_ring

variable n : ℕ

inductive symb : Type
| x : {i : ℕ // 1 ≤ i ∧ i ≤ n} → symb

def my_free_ring := free_ring $ symb n

--Lean complains if I don't do this
instance : ring $ my_free_ring n :=
begin
    unfold my_free_ring, apply_instance,
end

instance : module (my_free_ring n) (my_free_ring n) := by apply_instance

def my_ideal := submodule.span {x : my_free_ring n | true} --fails

/-
failed to synthesize type class instance for
n : ℕ
⊢ semiring ↥{x : my_free_ring n | true}

don't know how to synthesize placeholder
context:
n : ℕ
⊢ Type ?
-/

Why is Lean trying to coerce a set to semiring? What does the second error mean?

[Alex J. Best]

Well if you fix the first error the second might go away, so lets do that first. Lean is telling you that it is trying to interpret {x : my_free_ring n | true} as a semimodule which is because the function submodule.span takes a semimodule, the underlying module you are taking the submodule of, as its first argument, then a set of terms, so you probably want submodule.span (my_free_ring n) {x : my_free_ring n | true} instead.

[Kevin Buzzard]

@Zhangir Azerbayev are you sure you don't want to work with the "canonical" type of size n, namely fin n, rather than {i : ℕ // 1 ≤ i ∧ i ≤ n}? You only have one inequality to deal with, not two.

[Scott Morrison]

Regarding the first instance : ring (my_free_ring n) line --- you can just replace this by writing @[derive ring] before def my_free_ring.

[Scott Morrison]

It has exactly the same effect.

[Zhangir Azerbayev]

@Kevin Buzzard I wanted to start all my indices at 1 because that's how mathematicians do it, but 100 or so lines later I did realize that choice makes things cluttered and switched to fin n.

[Kevin Buzzard]

@Zhangir Azerbayev you are a quick learner :-)