Finite product of finite modules is finite

Stream: maths

[Riccardo Brasca]

In #10757 @Johan Commelin suggested to prove that a finite product of finite modules is finite (meaning the product over a fintype. Here finite means docs#module.finite). Does anyone have an idea on how to do it in Lean?

Mathematically there is nothing to prove, we have docs#module.finite.prod, so it is a trivial induction. But the only induction principle for fintype I found is docs#fintype.induction_empty_option, that is a little annoying. In any case I don't find anything about the product over option α, so one should prove that first.

Another annoying problem is that in this case we three construction: Π, Π₀ and ⨁: mathblib knows that they are (linearly) equivalent, but it makes searching the library a little complicated.

Any ideas? Thanks!

[Anne Baanen]

Biject the fintype to fin n (docs#fintype.equiv_fin) and do induction on n?

[Eric Wieser]

Do we have docs#submodule.pi (cf docs#submodule.prod) and docs#submodule.fg_pi (cf docs#submodule.fg_prod)

[Eric Wieser]

It looks like it would be straightforward to adjust the proof of fg_prod to produce fg_pi (probably easier than trying to do induction)

[Eric Wieser]

/-- The `pi` version of `linear_map.prod_eq_sup_map`. -/
lemma pi_eq_supr_map {ι : Type*} [decidable_eq ι] {s : set ι} {p : ι → submodule R M} :
  pi s p = ⨆ i ∈ s, map (linear_map.single i : _ →ₗ[R] _) (p i) :=
sorry -- similar to submodule.supr_map_single

theorem fg_pi {ι : Type*} {s : set ι} {p : ι → submodule R M} (hs : s.finite)
  (hsb : ∀ i ∈ s, (p i).fg) : (submodule.pi s p).fg :=
begin
  classical,
  simp_rw fg_def at hsb,
  choose t htf hts using hsb,
  refine fg_def.2 ⟨⋃ i ∈ s, (linear_map.single i : _ →ₗ[R] _) '' t i ‹_›,
    set.finite.bUnion hs $ λ i hi, (htf i hi).image _, _⟩,
  simp_rw [span_Union, span_image, hts, pi_eq_supr_map],
end

[Riccardo Brasca]

@Eric Wieser Thanks, this is probably the easiest way

[Eric Wieser]

I'm not actually sure that that sorry is true without a finite assumption

[Eric Wieser]

But that's fine for your application, because you have the assumption already in the other lemma

[David Wärn]

You could have a look at the proof of docs#is_artinian_pi to see how to prove this using the induction principle for fintype. In particular we do have docs#linear_equiv.pi_option_equiv_prod for the product over option A.

BTW one could implement another induction principle for fintype using sum instead of option. It might be easier to use for this.

[Riccardo Brasca]

Is there a reason why you work with a s : set ι with s.finite rather than with a fintype or a finset?

[Riccardo Brasca]

I mean, at the end all these notions are equivalent of course, but I am always a little bit confused by which one to use.

[Eric Wieser]

Is that aimed at me or David?

[Riccardo Brasca]

It was aimed at Eric, I didn't noticed David's answer

[Eric Wieser]

My statement was about s : set because that's what submodule.pi takes

[Eric Wieser]

And a statement of fg (pi s p) is (syntactically) more general than one about fg (pi ↑s p)

[Eric Wieser]

David Wärn said:

You could have a look at the proof of docs#is_artinian_pi to see how to prove this using the induction principle for fintype.

I'd argue that this probably should have been proved in the same way as the _prod version, as this exposes a bunch of lemma holes in the linear map API. Edit: oh, those holes aren't true

[Riccardo Brasca]

I have the feeling that the correct way of proving the result is as in docs#is_artinian_pi, but mabye this is because submodule.pi s p really confuses me

[Eric Wieser]

Ah, it looks like I was confused by submodule.pi too

[Eric Wieser]

It probably only makes sense to prove it about set.univ, which is easier anyway

[Riccardo Brasca]

Ah OK, submodule.pi is the product as a submodule of the product, so it makes sense to prove that the product of finitely many finitely generated submodules is finitely generated

[Eric Wieser]

I PR'd #10845

[Eric Wieser]

submodule.pi is a submodule of the pi type which is only constrained at the given indices

[Eric Wieser]

As opposed to how I read it, which is the submodule of the pi type which is only non-zero at the given indices

[Eric Wieser]

We're missing the analogous statement for subalgebras, though we're also missing subalgebra.pi needed to state it

[Riccardo Brasca]

For algebras we have both finite and finite_type. I can do it sooner or later