Submodule generated by two free submodules of a free module

Stream: new members

[Richard Copley]

Do we have the theorem in Mathlib that the submodule generated by two (or finitely many) free submodules of a free module is free? I can't even state it. I think there is a universe problem.

import Mathlib.LinearAlgebra.FreeModule.Basic

open Module

variable {R : Type*} [CommRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Free R M]

theorem Module.Free.sup (K₁ K₂ : Submodule R M) (h₁ : Free R K₁) (h₂ : Free R K₂):
    Free R (K₁ ⊔ K₂) := by
  --        ~~~~~~~
  -- failed to synthesize instance Sup (Type u_2)
  sorry

[Kevin Buzzard]

theorem Module.Free.sup (K₁ K₂ : Submodule R M) (h₁ : Free R K₁) (h₂ : Free R K₂):
    Free R (K₁ ⊔ K₂ : Submodule R M) := by

Lean needed more directions for the coercion.

[Richard Copley]

Great! This is about 14 levels deep in a complex of rabbit holes. I'll get started doing Steinitz exchange stuff. Maybe it will be fun.

[Reid Barton]

Isn't it not true though? e.g. $R = k[x,y]$, $M = R$, and the submodules $xM$, $yM$

[Kyle Miller]

Maybe you want to add in that $R$ is a PID?

[Richard Copley]

Reid Barton said:

Isn't it not true though? e.g. $R = k[x,y]$, $M = R$, and the submodules $xM$, $yM$

Forgive me, can you spell it out for me? I don't know what xM ⊔ yM is if it isn't the span of {x, y}. And {x, y} is linearly independent. What's missing?

[Reid Barton]

$x,y$ isn't linearly independent because $y \cdot x - x \cdot y = 0$.

[Richard Copley]

Thanks!

[Richard Copley]

Uh. But now what's the basis for k[x,y]?

[Reid Barton]

$M = R$ is free as an $R$-module, the basis is {1}.

[Richard Copley]

Super. Thanks for rescuing me.

Kyle Miller said:

Maybe you want to add in that $R$ is a PID?

That would do it, but I don't have it. There'll be something in the context that means I don't need this to be true.

[Richard Copley]

This weaker statement sufficed: if $K₁$ and $K₂$ are finitely generated $R$-submodules of a free $R$-module $M$, there exists a free, finitely generated $R$-submodule of $M$ which includes $K₁$ and $K₂$.

Proof

import Mathlib.LinearAlgebra.FreeModule.Basic
import Mathlib.RingTheory.Finiteness

variable (R : Type*) [CommRing R]
variable (M : Type*) [DecidableEq M] [AddCommGroup M] [Module R M] [Module.Free R M]
open Submodule

/-- If `K₁` and `K₂` are finitely generated `R`-submodules of a free `R`-module `M`, there
exists a free, finitely generated `R`-submodule of `M` which includes `K₁` and `K₂`. -/
theorem exists_fg_sup_le (K₁ K₂ : Submodule R M) (hfg₁ : K₁.FG) (hfg₂ : K₂.FG) :
    ∃ S : Finset M, LinearIndependent R ((↑) : S → M) ∧ K₁ ⊔ K₂ ≤ span R S := by
  obtain ⟨S₁, rfl⟩ := hfg₁
  obtain ⟨S₂, rfl⟩ := hfg₂
  let ⟨⟨ι, ℰ⟩⟩ := ‹Module.Free R M›
  haveI : DecidableEq ι := Classical.decEq ι
  let indices := (S₁ ∪ S₂).attach.sup fun s => (ℰ.repr s).support
  use indices.image ℰ
  rewrite [← span_union, span_le]
  constructor
  . have hf : ∀ x : indices.image ℰ, ∃ i : ι, ℰ i = x := fun ⟨_, hx⟩ =>
      match Finset.mem_image.mp hx with | ⟨i, _, hi⟩ => ⟨i, hi⟩
    choose f h using hf
    have hval : ((↑) : indices.image ℰ → M) = ℰ ∘ f := funext fun i => (h i).symm
    exact hval ▸ ℰ.linearIndependent.comp f fun x y hxy =>
      Subtype.ext (hval ▸ (id (congrArg ℰ hxy) : (ℰ ∘ f) x = (ℰ ∘ f) y))
  . intro s hs
    rewrite [← Finset.coe_union S₁ S₂, Finset.mem_coe] at hs
    unfold_let indices
    rewrite [SetLike.mem_coe, Finset.sup_eq_biUnion, Finset.coe_image,
        Finset.coe_biUnion, Set.image_iUnion₂, span_iUnion₂]
    exact mem_iSup_of_mem ⟨s, hs⟩
      (mem_iSup_of_mem (Finset.mem_attach (S₁ ∪ S₂) ⟨s, hs⟩)
        (Basis.mem_span_repr_support ℰ s))