is_submodule ?

Stream: Is there code for X?

[Michael Stoll]

Is there a way in mathlib to express the fact that a subset of a module is a submodule? I.e. something like

def is_submodule (R) {M} [semiring R] [add_comm_monoid M] [module R M] (S : set M) : Prop :=.
0 ∈ S ∧ ∀ (a b : M), a ∈ S → b ∈ S → a + b ∈ S ∧ ∀ (c : R) (x : M), x ∈ S → c • x ∈ S

(and then another def that constructs the actual submodule structure when this holds).

Of course, I can define it like this, but I would expect that this is somewhere in mathlib.

[Eric Wieser]

I would guess that S ∈ set.range (coe : submodule R M → set M) would be most useful

[Michael Stoll]

As the definition of is_submodule, you mean?

[Eric Wieser]

Yes, because then you can more easily promote it to a submodule. What's the application here?

[Michael Stoll]

I would like to express that some set is a linear subspace in a theorem statement, and what you propose is rather opaque.

[Eric Wieser]

Normally the approach taken is

def foo : set M := ...

def foo_submodule [extra_assumptions_on M] : submodule R M :=
{ carrier := foo M, ... }

lemma coe_foo_submodule : ↑foo_submodule = foo := rfl

[Michael Stoll]

The statement says something like "under such and such assumptions, there is a certain subset of \F_2^n that is a linear subspace".

[Eric Wieser]

Right, I think the above is how we currently handle that

[Eric Wieser]

That is, rephase it as "we define certain_submodule, which is certain_subset as a submodule"

[Eric Wieser]

See for instance docs#set.center, docs#submonoid.center

[Michael Stoll]

But how do you phrase "there is a S : set M with certain properties that is a submodule".
I cannot define the set, I want to assert its existence.

[Eric Wieser]

What statement would you like to be able to write?

[Eric Wieser]

Something like ∃ s : set M, is_submodule s ∧ has_properties s?

[Michael Stoll]

Right.

[Eric Wieser]

Just write ∃ s : submodule R M, has_properties (s : set M)

[Eric Wieser]

Then s is a submodule by construction

[Michael Stoll]

OK, that should work. It requires some additional contortion (since s here has a specific form, so I have to express that via the has_properties part), but should be OK.

[Eric Wieser]

I would be surprised if the contortion is more than a coe here or there.

[Eric Wieser]

Is your actual case more like ∃ x : X, is_submodule (f x) ∧ has_properties x?

[Michael Stoll]

To un- #xy, the statement I want to formalize is
"Let Z₀, …, Zₜ ⊆ 𝔽₂ⁿ be non-singleton subsets that each contain 0. If all tuples of vectors in Z₀ × ⋯ × Zₜ are linearly dependent, then there exists a subset I ⊆ {0, …, t} such that the partial sumset ∑_{i∈I} Zᵢ is a nontrivial subspace of 𝔽₂ⁿ."

So my s is a pointwise sum of subsets, and the quantifier is for the index subset.

The next question is how to write the sum of subsets...

[Michael Stoll]

What I have so far is this:

open_locale pointwise

@[reducible] def M (n : ℕ) : Type := fin n → zmod 2

variables {n : ℕ}

theorem prop_2_4 {ι} (Z : ι → set (M n))
  (h₀ : ∀ i : ι, (0 : M n) ∈ Z i) (h₁ : ∀ i : ι, ∃ v ∈ Z i, v ≠ 0)
  (hld : ∀ b : ι → (M n), ∀ i : ι, b i ∈ Z i → ¬ linear_independent (zmod 2) b) :
∃ (I : set ι) (V : submodule (zmod 2) (M n)), V ≠ ⊥ ∧ (V : set (M n)) = ∑ (i in I), Z i :=

but I get an "unexpected token" error at the sum sign.

[Michael Stoll]

∃ (I : finset ι) (V : submodule (zmod 2) (M n)), V ≠ ⊥ ∧ (V : set (M n)) = I.sum Z := at least removes the error.
Now I have to see whether I can formalize the proof...

[Eric Wieser]

open_locale big_operators is needed to make \sum work as notation

[Eric Wieser]

And it's ∑ i in I, f i not ∑ (i in I), f i

[Eric Wieser]

Let Z₀, …, Zₜ ⊆ 𝔽₂ⁿ be non-singleton subsets that each contain 0.

Perhaps I'm being stupid, but isn't every such subset a submodule?

[Michael Stoll]

No. Take {0, e_1, e_2}, where e_1, e_2 are linearly independent (and n is at least 2).

[Eric Wieser]

Your statement looks sensible to me then

[Michael Stoll]

Thanks for reminding me of open_locale big_operators and the correct syntax. It is easy to forget stuff that one doesn't use on a daily basis...

[Eric Wieser]

I think your statement is false if iota is empty

[Michael Stoll]

OK. I'll add [nonempty \iota] [finite \iota]...

[Eric Wieser]

I think ∀ i : ι, b i ∈ Z i → ¬ linear_independent (zmod 2) b should be (∀ i : ι, b i ∈ Z i) → ¬ linear_independent (zmod 2) b too

[Eric Wieser]

In fact, I think that makes it true again for the empty type

[Michael Stoll]

1) Thanks! 2) No, since the subspace would be trivial then.

[Michael Stoll]

Now I'm struggling with stating that the dimension of the span of some subset is one less than the cardinality of \iota.
My attempt module.rank ↥(submodule.span (zmod 2) (set.range b)) + 1 = cardinal.mk ι produces a "type mismatch" error that I find hard to parse.

[Eric Wieser]

Michael Stoll said:

2) No, since the subspace would be trivial then.

But isn't hld impossible in that case since all empty vectors are linearly independent? So the statement is true by eliminating using hld.

[Michael Stoll]

Ah, OK; I guess you are right!

[Michael Stoll]

Here is the error message:

type mismatch at application
  module.rank ↥(submodule.span (zmod 2) (set.range b)) + 1 = cardinal.mk ι
term
  cardinal.mk ι
has type
  cardinal : Type (?+1)
but is expected to have type
  Π (V : Type ?) [_inst_1 : semiring ↥(submodule.span (zmod 2) (set.range b))] [_inst_2 : add_comm_monoid V]
  [_inst_3 : module ↥(submodule.span (zmod 2) (set.range b)) V], cardinal : Type (?+1)

I have to confess that I have no idea what this wants to tell me...

[Eric Wieser]

It tells you that you wrote an equality of functions by accident

[Eric Wieser]

Because you missed an argument to docs#module.rank

[Michael Stoll]

It is a bit annoying that I have to carry around the base ring everywhere...

[Eric Wieser]

In Lean's defence, ↥(submodule.span (zmod 2) (set.range b)) is also a nat-module, an int-module, ...