Zulip Chat Archive

Stream: maths

Topic: Finite product of finite modules is finite


Riccardo Brasca (Dec 16 2021 at 09:44):

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 (Dec 16 2021 at 10:55):

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

Eric Wieser (Dec 16 2021 at 11:16):

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

Eric Wieser (Dec 16 2021 at 11:17):

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 (Dec 16 2021 at 11:29):

/-- 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 (Dec 16 2021 at 13:40):

@Eric Wieser Thanks, this is probably the easiest way

Eric Wieser (Dec 16 2021 at 13:47):

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

Eric Wieser (Dec 16 2021 at 13:48):

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

David Wärn (Dec 16 2021 at 14:14):

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 (Dec 16 2021 at 14:14):

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

Riccardo Brasca (Dec 16 2021 at 14:14):

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 (Dec 16 2021 at 14:15):

Is that aimed at me or David?

Riccardo Brasca (Dec 16 2021 at 14:16):

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

Eric Wieser (Dec 16 2021 at 14:16):

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

Eric Wieser (Dec 16 2021 at 14:17):

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

Eric Wieser (Dec 16 2021 at 14:30):

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 (Dec 16 2021 at 14:40):

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 (Dec 16 2021 at 15:00):

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

Eric Wieser (Dec 16 2021 at 15:00):

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

Riccardo Brasca (Dec 16 2021 at 15:06):

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 (Dec 16 2021 at 15:09):

I PR'd #10845

Eric Wieser (Dec 16 2021 at 15:10):

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

Eric Wieser (Dec 16 2021 at 15:10):

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 (Dec 17 2021 at 17:34):

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

Riccardo Brasca (Dec 17 2021 at 18:45):

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


Last updated: Dec 20 2023 at 11:08 UTC