Proper subspace contained in maximal subspace?

Stream: Is there code for X?

[Kevin Buzzard]

import Mathlib

-- let k be a field
variable {k : Type*} [Field k]
-- let V be a fdvs over k
variable {V : Type*} [AddCommGroup V] [Module k V] [FiniteDimensional k V]
-- let W be a proper subspace of V
variable (W : Submodule k V) (hW : W ≠ ⊤)


-- Then W is contained in a hyperplane
-- I don't care how to say this, I could work with anything
open Submodule in
example : ∃ (X : Submodule k V) (z : V),
    W ≤ X ∧ z ≠ 0 ∧ Disjoint W (span k {z}) ∧ W ⊔ span k {z} = ⊤ := sorry

open FiniteDimensional in
example : ∃ X : Submodule k V, W ≤ X ∧ finrank k X + 1 = finrank k V := sorry

-- attempt to apply some fancy Zorn thing
#synth IsCoatomic (Submodule k V) -- fails :-(

[Antoine Chambert-Loir]

what if you add that V is nontrivial ?

[Antoine Chambert-Loir]

import Mathlib

-- let k be a field
variable {k : Type*} [Field k]
-- let V be a vector space over k
variable {V : Type*} [AddCommGroup V] [Module k V]

example : IsCoatomic (Submodule k V) :=
  isCoatomic_of_isAtomic_of_complementedLattice_of_isModular

[Antoine Chambert-Loir]

The proof does not use finite dimensionality, but the semisimplicity of vector spaces !!

[Kevin Buzzard]

Aah of course -- I had "added the nontriviality" with the existence of W but of course typeclass inference can't see this. Thanks!

[Antoine Chambert-Loir]

Over a ring, you need the hypothesis that the module is noetherian.

import Mathlib

variable {k : Type*} [Semiring k]
variable {M : Type*} [AddCommMonoid M] [Module k M]
variable [Nontrivial M]

example (hM : IsNoetherian k M): IsCoatomic (Submodule k M) := by
  rw [isNoetherian_iff_wellFounded] at hM
  exact isCoatomic_of_orderTop_gt_wellFounded hM

[Kevin Buzzard]

I've come back to this and realised that I can't find any results linking coatoms in finite-dimensional vector spaces to codimension 1 subspaces. I've come up with the following horrible proof that an n+1-dimensional space contains an n-dimensional subspace. How should I have done this?

import Mathlib

variable {k : Type*} [Field k]
variable {V : Type*} [AddCommGroup V] [Module k V] [FiniteDimensional k V]

open FiniteDimensional

lemma foo (n : ℕ) (hV : finrank k V = n + 1) : ∃ W : Submodule k V, finrank k W = n := by
  let B := IsNoetherian.finsetBasis k V
  have h := FiniteDimensional.finrank_eq_card_basis B
  let C : Basis (Finset.range (n + 1)) k V := Basis.reindex B <| Fintype.equivOfCardEq ?_
  · let g : Fin n → {x // x ∈ Finset.range (n + 1)} := fun i => ⟨i.1, by
      have := i.2
      rw [Finset.mem_range]
      omega⟩
    use Submodule.span k (Set.range (C ∘ g))
    suffices finrank k ↥(Submodule.span k (Set.range (C ∘ g))) = Fintype.card (Fin n) by
      convert this
      exact (Fintype.card_fin n).symm
    apply finrank_span_eq_card _
    apply LinearIndependent.comp
    · exact Basis.linearIndependent C
    · intro ⟨x1, hx1⟩ ⟨x2, hx2⟩ h
      simp_all
  · rw [← h, ← hV]
    simp

[Antoine Chambert-Loir]

I used noetherian, but finitely generated was all that was needed. Now, if you have a maximal submodule, you have to use that the quotient is a simple module and know about them. In particular any nonzero element is a generator. For vector spaces, that means dim 1.

[Kevin Buzzard]

Yes I'm sure that's a more elegant way to do it. @Lucas Whitfield instead of that horrible proof we just constructed, you might want to prove that the quotient by a coatom is simple and go that way.

[Junyan Xu]

I can't find any results linking coatoms in finite-dimensional vector spaces to codimension 1 subspaces

We have docs#isSimpleModule_iff_isCoatom and we should make docs#is_simple_module_of_finrank_eq_one an iff (edit: when K = A)

[Kevin Buzzard]

Oh nice! Yeah this approach is much more elegant:

import Mathlib

variable {k : Type*} [Field k]
variable {V : Type*} [AddCommGroup V] [Module k V] [FiniteDimensional k V]

open FiniteDimensional

instance : IsCoatomic (Submodule k V) :=
  isCoatomic_of_isAtomic_of_complementedLattice_of_isModular

lemma finrank_eq_one_of_isSimpleModule [IsSimpleModule k V] : finrank k V = 1 := by
  have : Nontrivial V := IsSimpleModule.nontrivial k V
  obtain ⟨v, hv⟩ := exists_ne (0 : V)
  rw [finrank_eq_one_iff_of_nonzero v hv]
  obtain (h | h) := eq_bot_or_eq_top <| Submodule.span k {v}
  · simp_all [Submodule.span_singleton_eq_bot]
  · assumption

lemma baz (n : ℕ) (hV : finrank k V = n + 1) (X : Submodule k V) (hX : X ≠ ⊤) :
    ∃ W : Submodule k V, X ≤ W ∧ finrank k W = n := by
  obtain (h1 | ⟨W, hW1, hW2⟩) := eq_top_or_exists_le_coatom X; contradiction
  use W, hW2
  rw [← isSimpleModule_iff_isCoatom] at hW1
  apply finrank_eq_one_of_isSimpleModule at hW1
  have := W.finrank_quotient_add_finrank
  omega

[Junyan Xu]

I've added

theorem isSimpleModule_iff_finrank_eq_one {R} [DivisionRing R] [Module R M] :
    IsSimpleModule R M ↔ FiniteDimensional.finrank R M = 1 :=

to #10808.