universe question: module.free

Stream: general

[Fabian Glöckle]

According to the definition of module.free, the index set of a basis has to live in the same universe as the module. Is this necessary?
I am asking because I do not see a way of resolving this problem:

type mismatch at application
  sigma.mk h.some
term
  h.some
has type
  Type (u_2+1) : Type (u_2+2)
but is expected to have type
  Type u_2 : Type (u_2+1)
state:
R : Type u_1,
_inst_1 : comm_ring R,
M : Type u_2,
_inst_2 : add_comm_group M,
_inst_3 : module R M,
_inst_4 : is_domain R,
_inst_5 : is_principal_ideal_ring R,
N : submodule R M,
_inst_6 : module.free R M,
h : ∃ (B : Type (u_2+1)), nonempty (basis B R ↥N)
⊢ module.free R ↥N

CanI resolve the problem by mapping the basis with the basis map to a subset of N?
Or should the definition of module.free be changed?

I am trying to prove

@[instance]
theorem submodule.free_of_pid_of_free [is_domain R] [is_principal_ideal_ring R] {N : submodule R M}
  [module.free R M] :
module.free R N :=
begin
  have h := submodule.nonempty_basis_of_pid' (module.free.choose_basis R M) N,
  exact ⟨⟨⟨h.some, h.some_spec⟩⟩⟩
end

using a

submodule.nonempty_basis_of_pid' :
  ∀ {R : Type u_4} [_inst_1 : comm_ring R] {M : Type u_5} [_inst_2 : add_comm_group M] [_inst_3 : module R M]
  [_inst_4 : is_domain R] [_inst_5 : is_principal_ideal_ring R] {ι : Type u_3},
    basis ι R M → ∀ (N : submodule R M), ∃ (B : Type (u_3+1)), nonempty (basis B R ↥N)

[Anne Baanen]

Maybe docs#basis.reindex_range helps here?

[Fabian Glöckle]

yiha, yes!

[Fabian Glöckle]

@[instance]
theorem submodule.free_of_pid_of_free [is_domain R] [is_principal_ideal_ring R] {N : submodule R M}
  [module.free R M] :
module.free R N :=
begin
  have h := submodule.nonempty_basis_of_pid' (module.free.choose_basis R M) N,
  let B := h.some,
  have hB := h.some_spec,
  cases hB,
  let b := basis.reindex_range hB,
  exact ⟨⟨⟨↥(set.range ⇑hB), b⟩⟩⟩,
end

[Anne Baanen]

So it's not necessary that the index set lives in the same universe, but it is convenient since otherwise we'd have a free universe parameter. And with docs#basis.reindex_range you can always get a basis to live in the correct universe.

[Anne Baanen]

Note that docs#module.free.of_basis already does this for you

[Fabian Glöckle]

ah :D I'm reinventing the wheel

[Fabian Glöckle]

the better!

[Riccardo Brasca]

I am on my phone at the moment, but I am almost sure I was pretty careful to state everything in full generality concerning universes. There was a reason I don't remember for having the definition like that and then the theorem rather than the other way.