Lattice (module)

Stream: Is there code for X?

[Eloi Torrents]

Is there code for this kind of lattices? https://en.m.wikipedia.org/wiki/Lattice_(module)

I'm interested in proving things about its endomorphisms...

[Kevin Buzzard]

That definition does not exist in Lean (as far as I know), but it would not be difficult to make.

[Yaël Dillies]

Yup, we have all the ingredients for it.

[Yury G. Kudryashov]

You can just use something like submodule int E

[Eloi Torrents]

Is this definition good enough to get started?

import ring_theory.localization

instance module_of_subring (R : Type*) (K: Type*) (V: Type*)
    [integral_domain R][field K] [algebra R K] [is_fraction_ring R K]
    [add_comm_group V] [module K V]: module R V :=
    by sorry

structure module.lattice (R : Type*) (K: Type*) (V: Type*)
    [integral_domain R][field K] [algebra R K] [is_fraction_ring R K]
    [add_comm_group V] [module K V]
    :=
  (carrier : submodule R V)
  (B: finset carrier)
  (is_basis: basis B R carrier)

I'm not sure if this should be a structure or a class, if I should use parameters or the keyword "extends", ...

[Eric Wieser]

I think your module_of_subring might just be docs#submodule.restrict_scalars?

[Eric Wieser]

But since it carries data it's not the only way to fill that sorry

[Eloi Torrents]

I figured out that what I need is [is_scalar_tower R K V]. This needs an instance [has_scalar R V], I made one, but Lean doesn't find it...

import ring_theory.localization

instance has_scalar_R_V (R : Type) (K: Type) (V: Type)
    [integral_domain R] [field K] [algebra R K] [is_fraction_ring R K]
    [add_comm_group V] [module K V] : has_scalar R V :=
    { smul := λ r v, _inst_3.to_fun r • v}

structure module.lattice (R : Type*) (K: Type*) (V: Type*)
    [integral_domain R][field K] [algebra R K] [is_fraction_ring R K]
    [add_comm_group V] [module K V] [is_scalar_tower R K V]
    :=
  (carrier : submodule R V)
  (B: finset carrier)
  (is_basis: basis B R carrier)

    /-
    failed to synthesize type class instance for
    R : Type ?,
    K : Type ?,
    V : Type ?,
    _inst_1 : integral_domain R,
    _inst_2 : field K,
    _inst_3 : algebra R K,
    _inst_4 : is_fraction_ring R K,
    _inst_5 : add_comm_group V,
    _inst_6 : module K V
    ⊢ has_scalar R V
    -/