f.g. free modules

Stream: maths

[Kevin Buzzard]

I'm trying to catch up with this thread. I am confused by this doesn't work:

import linear_algebra.basic tactic linear_algebra.basis linear_algebra.direct_sum_module

variable (ι : Type*)

open_locale classical

variables (R : Type*) [comm_ring R]

--noncomputable instance foo : module R (direct_sum ι (λ _:ι, R)) := by apply_instance

noncomputable example (x : direct_sum ι (λ _:ι, R)) (r : R) : direct_sum ι (λ _:ι, R) := r • x

If I comment out the instance, which apparently is already there, it works.

[Sam Lichtenstein]

I didn’t know I could fix this error by writing “noncomputable” before example

[Kevin Buzzard]

You still get the error with the smul, but if I comment out the instance it fixes it

[Kevin Buzzard]

OK so I'm catching up with the issues raised in this thread. direct_sum is for an arbitrary direct sum of $R$-modules (and in particular is a dependent finsupp). This specific case of free $R$-modules is somehow easier because it's not dependent, but there is a cost to introducing a new definition like free: Kenny's suggestion of just using ι →₀ R has advantages and disadvantages. On the other hand the concept of a free module is so ubiquitous that probably one has to make the definition.

The second point is that I suspect there's no coercion from finset to Type :-(

example (X : Type) : has_coe_to_sort (finset X) := by apply_instance -- fails

There's a coercion from finset X to set X and then from there to Type*, but I don't seem to be able to get there directly.

example (X : Type) (s : finset X) : Type := (↑s : set X)

Should there be a coercion from finset X to Type directly?

[Johan Commelin]

We could define free in terms of ι →₀ R

[Johan Commelin]

I often write { x // x \in s }. But of course that's a very roundabout way to make a Type out of a finset

[Sam Lichtenstein]

Kevin, how should I think about the "cost" of introducing a new definition? Is the point that this is just one more thing that needs to be unfolded, so it introduces some fixed amount of overhead for simp etc in all downstream code?

[Sam Lichtenstein]

I guess another question I had was whether all the free constructions in algebra.* should be special cases of a general definition (involving adjoints to forgetful functors), and their concrete descriptions (e.g. free module = direct sum or finitely supported functions or whatever) should be lemmas rather than definitions

[Patrick Massot]

Why is this conversation in "new members" rather than maths? It seems to be far beyond the newbie question about proving $P \wedge Q \implies Q \wedge P$.

[Notification Bot]

This topic was moved here from #new members > f.g. free modules by Rob Lewis

[Kevin Buzzard]

Another thing about introducing a terminology for ι →₀ R is that Lean will then have to be told that it's e.g. a module.

[Reid Barton]

I think we already have a characteristic predicate for "M is the free R-module on a set S", only we call it instead "S is an R-basis of the R-module M".

[Kenny Lau]

@_Notification Bot|100006 said:

This topic was moved here from #new members > f.g. free modules by Rob Lewis

hey we can do that??!!

[Kevin Buzzard]

Reid Barton said:

I think we already have a characteristic predicate for "M is the free R-module on a set S", only we call it instead "S is an R-basis of the R-module M".

My understanding of the original question is that basically it is how to prove that if M is a finitely-generated (so in particular there's some S : finset M which is known to span) then it admits a surjection from an f.g. free module. One issue is that S here has type finset M, so you do need to build some kind of free module with something resembling S as a basis, and then it will all be easy. The question is how to build this free module in an idiomatic way.

[Sam Lichtenstein]

@Reid Barton yes, I agree with that. but then when you use the "object" that is the free module on ι, it should be convenient to get your hands on:

def std_basis (i:ι) := direct_sum.lof R ι (λ _:ι, R) i 1 -- this is the std basis if we are working with direct_sum ι (λ _:ι, R)) as the free R-module on ι

lemma is_basis_std_basis : is_basis R (std_basis R ι) := sorry

(I know that lemma is not so hard to prove, but the proof doesn't seem to be as easy as simp given the lemma of the same name in linear_algebra/basis.lean.)

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/f142b4208bee350d00931b9fa38069cc740c83ef/src/linear_algebra/finsupp_vector_space.lean#L52-L54

lemma is_basis_single {φ : ι → Type*} (f : Π ι, φ ι → V)
  (hf : ∀i, is_basis K (f i)) :
  is_basis K (λ ix : Σ i, φ i, single ix.1 (f ix.1 ix.2)) :=

[Sam Lichtenstein]

Doesn't seem like that lemma should need [field K], right?

[Reid Barton]

Right, so while the characterization of being a free module is more or less under control, the construction of free modules is lacking, at a minimum, a coherent API. "The free R-module on a set" is far too important a notion to give the cryptic notation ι →₀ R, in my opinion.

[Sam Lichtenstein]

I don't suppose the parser could handle the notation $\bigoplus_\iota R$, assuming we could type that in Unicode easily?

[Sam Lichtenstein]

or $R^{\oplus \iota}$ I suppose

[Johan Commelin]

@Sam Lichtenstein That first suggestion shouldn't be a problem

[Johan Commelin]

It would basically be

notation `\bigoplus` := direct_sum

[Johan Commelin]

@Sam Lichtenstein Concerning your question about the cost of adding a def.

1. You certainly don't have to worry about what lean the program thinks about a new def. It sees thousands of them every day, and it won't loose any sleep over seeing yet another one.

2. You might worry about the 'social contract' that comes with add a def to mathlib. Namely, that you should also provide a (bare minimum) API. You'll have to sit down, and think of all the stupid, silly, trivial statements that a mathematician would not write down in a textbook chapter on that new definition. And then state and prove all those stupid, silly, trivial lemmas.

As Reid said above: free is certainly so fundamental that it deserves being a definition.

[Sam Lichtenstein]

apparently \bigoplus is not in the unicode character set. what about ∐ (as distinct from the infix operator ⨿ for binary coproducts)

[Johan Commelin]

Hmmm... maybe we should just implement LaTeX mode for lean

[Johan Commelin]

:fire: burn unicode to the ground :fire:

[Johan Commelin]

Is Tom Hales's CNL already usable is input language for lean?

[Johan Commelin]

@Jesse Michael Han @Floris van Doorn do you have any news from the front?

[Reid Barton]

I found ⨁ U+2A01 N-ARY CIRCLED PLUS OPERATOR (not to be confused with ⊕ U+2295 CIRCLED PLUS)

[Reid Barton]

In case of emergency there's also ⴲ U+2D32 TIFINAGH LETTER YABH

[Johan Commelin]

That's \slightlybiggerthannormaloplus

[Sam Lichtenstein]

ah I see --- it lives in 'Supplemental Mathematical Operators"

[Bryan Gin-ge Chen]

⨁ U+2A01 N-ARY CIRCLED PLUS OPERATOR should be \O+ in vscode-lean.

[Sam Lichtenstein]

OK i took a stab at coming up with an API for free modules. It's mostly just specializing Kenny's direct_sum API to the non-dependent case. (I am sure there are things I could improve upon stylistically...)

However, the "punchline" lemma free.surj_of_fg still seems surprisingly hard to prove, because of the difficulties Kevin noted regarding coercion between various subset types. I have an outline of the proof at the bottom below. Unfortunately, at the key moment, the transitivity tactic fails to work for reasons that are mysterious to me.

import linear_algebra.basic
       linear_algebra.direct_sum_module
       linear_algebra.basis
       linear_algebra.finsupp_vector_space
       ring_theory.noetherian
       data.finsupp
       tactic

section

open_locale classical

def free (R:Type*) (ι:Type*) [comm_ring R][decidable_eq ι] := direct_sum ι (λ _:ι, R)

universes u v w u₁

variables (R : Type u) [comm_ring R]
variables (ι : Type v) [decidable_eq ι]
notation `⨁[`:500 ι:25 `] `:0 R := free R ι

instance free.add_comm_group : add_comm_group ⨁[ι] R  := direct_sum.add_comm_group
example (x y : ⨁[ι] R) : ⨁[ι] R := x + y
instance free.module : module R ⨁[ι] R := direct_sum.module
example (x : ⨁[ι] R) (r : R) : ⨁[ι] R := r • x

variables {R ι}

abbreviation free.to_module {M : Type*} [add_comm_group M] [module R M] :
   (ι → (R →ₗ[R] M))  →  (⨁[ι] R) →ₗ[R] M :=
   direct_sum.to_module R ι M
abbreviation free.component : Π (i:ι), (⨁[ι] R) →ₗ[R] R :=
     direct_sum.component R ι (λ _:ι, R)

@[ext] lemma free.ext {f g : ⨁[ι] R}
  (h : ∀ i, free.component i f = free.component i g) : f = g :=
  @direct_sum.ext R _ ι _ (λ _:ι, R) _ _ f g h

lemma free.ext_iff {f g : ⨁[ι] R} : f = g ↔
  ∀ i, free.component i f = free.component i g :=
begin
split, intros h i, rw h, ext,
end

abbreviation free.lof : ι → R →ₗ[R] ⨁[ι] R := direct_sum.lof R ι (λ _:ι, R)

def free.std_basis (i:ι) := free.lof i (1:R)

@[simp] noncomputable def free.to_finsupp (x : ⨁[ι] R) : (ι →₀ R) :=
{ support := dfinsupp.support x,
  to_fun  := λ i, free.component i x,
  mem_support_to_fun := by {finish}}

def free.of_finsupp (f : ι →₀ R) := (finsupp.support f).sum(
    λ i, f i • @free.std_basis R _ ι _ i
)

-- kronecker delta on ι with values in R
@[simp] def δ (i j : ι) : R := ite (j = i) (1:R) 0

@[simp] lemma free.apply_eq_component (x : ⨁[ι] R) (i :ι) :
    free.to_finsupp x i = free.component i x := rfl

@[simp] lemma comp_std_basis (i j : ι) :
 (free.component i) (free.std_basis j) = @δ R _ ι _ i j :=
 begin rw δ, split_ifs with h,
{rw [h, free.std_basis, direct_sum.component.lof_self]},
{have H := @direct_sum.component.of R _ ι _ (λ _:ι, R) _ _ i j 1,
 simp only [eq_rec_constant] at H,
 have : (direct_sum.component R ι (λ (_x : ι), R) i) = (free.component i) := rfl,
 rw this at H,
 rw free.std_basis,
 replace this : (direct_sum.lof R ι (λ (_x : ι), R) j) = free.lof j := rfl,
 rw this at H,
 rw H, finish}
end

noncomputable lemma free.equiv_finsupp : (⨁[ι] R) ≃ₗ[R] ι →₀ R := {
    to_fun  := free.to_finsupp,
    add     := by {intros x y, ext1, induction x, induction y, all_goals {refl}},
    smul    := by {intros _ x, ext1, induction x, all_goals {refl}},
    inv_fun := free.of_finsupp,
  left_inv  := begin intro x, rw free.ext_iff, intro i,
        rw [free.of_finsupp, linear_map.map_sum (free.component i)],
        simp only [algebra.id.smul_eq_mul, comp_std_basis, linear_map.map_smul, δ,
                   mul_boole, finset.sum_ite_eq', finsupp.mem_support_iff, ne.def],
        split_ifs; tauto end,
  right_inv := begin intro f, ext i,
        suffices : (free.component i) (free.of_finsupp f) = f i, {tauto},
        rw [free.of_finsupp, linear_map.map_sum (free.component i)],
        simp only [mul_boole, algebra.id.smul_eq_mul, finset.sum_ite_eq', δ,
            finsupp.mem_support_iff, comp_std_basis, ne.def,
            linear_map.map_smul],
        split_ifs; finish end}

lemma is_basis_std_basis : @is_basis ι R (⨁[ι] R) free.std_basis _ _ _ :=
begin
rw is_basis, split,
-- linear independence
{rw linear_independent_iff', intros, rw free.ext_iff at a, replace a := a i,
simp only [linear_map.map_zero, comp_std_basis, smul_eq_mul, linear_map.map_sum, linear_map.map_smul, δ] at *, finish},
-- span
{rw submodule.span, simp only [Inf_eq_top, set.mem_set_of_eq] at *, intros,
ext1, split, tauto, intros hx, cases hx,
replace H : ∀ (i:ι), free.std_basis i ∈ a := by
        {intro, apply H, fconstructor, from i, refl},
apply direct_sum.induction_on x,
    {finish},
    {intros i r, have Hi := H i,
    suffices : free.lof i r ∈ a, {tauto},
    rw [← mul_one r, ← smul_eq_mul, linear_map.map_smul],
    from a.smul_mem r Hi},
    {intros y z, from a.add_mem}}
end

variables {M : Type v} [add_comm_group M] [module R M]

variables (R)
lemma lmap_of_elt.smul (m : M):
     ∀ (c x : R), (λ (r : R), r • m) (c • x) = c • (λ (r : R), r • m) x
:= begin intros r s, simp only [algebra.id.smul_eq_mul, mul_smul] at *, end
def lmap_of_elt (m : M): R →ₗ[R] M :=
    linear_map.mk (λ (r:R), r•m) (λ x y, add_smul x y m) (lmap_of_elt.smul R m)
lemma elt_of_lmap_of_elt_of_one (m : M) : m = lmap_of_elt R m (1:R) :=
begin rw lmap_of_elt, simp only [linear_map.coe_mk, one_smul] end

def lmap_of_elts (m : ι → M) : (⨁[ι] R) →ₗ[R] M :=
free.to_module (λ (i:ι), lmap_of_elt R (m i))
#check @lmap_of_elts R _ ι _ M _ _
#check lmap_of_elts R

lemma needs_a_name (m : ι → M) (i : ι) :
    (lmap_of_elts R m) (free.std_basis i) = m i :=
begin
rw lmap_of_elts, rw free.std_basis, simp only [direct_sum.to_module_lof],
from (elt_of_lmap_of_elt_of_one R (m i)).symm
end

variables (M)
variables {R}
-- set_option trace.simplify.rewrite true
lemma free.surj_of_fg (hfg : (⊤ : submodule R M).fg) :
    ∃ (ι : Type v) [fintype ι], ∃ (π : (⨁[ι] R) →ₗ[R] M), function.surjective π  :=
begin
cases hfg with s hs,
let ι₀ : set M := ↑s, let ι  : Type v := ↥ι₀,
use ι, fconstructor, {apply_instance},
let π₀ : ι → M := λ i, i,
let π := lmap_of_elts R π₀,
fconstructor, {use π},
{let πι := π '' set.range (@free.std_basis R _ ι _),
have Rπι_eq_πRι :=
    @submodule.span_image R (⨁[ι] R) M _ _ _ _ _ (set.range free.std_basis) π,
replace  Rπι_eq_πRι : submodule.span R πι = submodule.map π ⊤ := by
    {rw ← (@is_basis_std_basis R _ ι _).2, exact Rπι_eq_πRι},
intro m, have : m ∈ (⊤ : submodule R M) := by {tauto}, rw ← hs at this,
 rw submodule.mem_span at this, replace this := this (submodule.span R πι),
 have foo := @submodule.subset_span R M _ _ _ πι,
 have s_le_πι : ↑s ⊆ πι :=
 begin
    suffices : ∀ (i ∈ s), i ∈ πι, {tauto},
    intros i₀ hi₀,
    let i : ι := begin fconstructor, use i₀, tauto end,
    let πi := π (@free.std_basis R _ ι _ (i:ι)),
    suffices : i₀ = πi,
        {rw this,
        replace this := set.image_eq_range π (set.range free.std_basis),

        have baz := (@set.mem_range M (set.range (@free.std_basis R _ ι _)) (λ (x : ↥(set.range free.std_basis)), π x.val) πi).mpr,

        suffices : (∃ (y : (set.range (@free.std_basis R _ ι _))), (λ (x : (set.range (@free.std_basis R _ ι _))), π x.val) y = πi),
            {sorry},
        let y := @free.std_basis R _ ι _ i, use y,
        rw set.mem_range, use i},
    have : πi = π₀ i :=
        begin
            have := @needs_a_name R _ ι _ M _ _ π₀ i, finish,
        end,
    rw this,
    replace this : π₀ i = i := rfl,
    rw this, refl,
 end,
 have : m ∈ submodule.span R πι :=
 begin
    apply this, -- transitivity, -- does not work for some reason
    sorry
 end,
 -- should be easy to finish from here
 sorry,
}
end

end

[Sam Lichtenstein]

I got the proof of the last lemma to work by manually doing the transitivity. I also put all the free.* lemmas/definitions inside a namespace, which I assume is the right thing to do. See below for the version with these corrections. The proof of surj_of_fg is still way too painful for what it is, though, so I welcome suggestions if anyone has some.

import linear_algebra.basic
       linear_algebra.direct_sum_module
       linear_algebra.basis
       linear_algebra.finsupp_vector_space
       ring_theory.noetherian
       data.finsupp
       tactic


open_locale classical

def free (R:Type*) (ι:Type*) [comm_ring R][decidable_eq ι] := direct_sum ι (λ _:ι, R)

namespace free

universes u v w u₁

variables (R : Type u) [comm_ring R]
variables (ι : Type v) [decidable_eq ι]
notation `⨁[`:500 ι:25 `] `:0 R := free R ι


instance : add_comm_group ⨁[ι] R  := direct_sum.add_comm_group
example (x y : ⨁[ι] R) : ⨁[ι] R := x + y
instance : module R ⨁[ι] R := direct_sum.module
example (x : ⨁[ι] R) (r : R) : ⨁[ι] R := r • x

variables {R ι}

abbreviation to_module {M : Type*} [add_comm_group M] [module R M] :
   (ι → (R →ₗ[R] M))  →  (⨁[ι] R) →ₗ[R] M :=
   direct_sum.to_module R ι M
abbreviation component : Π (i:ι), (⨁[ι] R) →ₗ[R] R :=
     direct_sum.component R ι (λ _:ι, R)

@[ext] lemma ext {f g : ⨁[ι] R}
  (h : ∀ i, component i f = component i g) : f = g :=
  @direct_sum.ext R _ ι _ (λ _:ι, R) _ _ f g h

lemma ext_iff {f g : ⨁[ι] R} : f = g ↔
  ∀ i, component i f = component i g :=
begin
split, intros h i, rw h, ext,
end

abbreviation lof : ι → R →ₗ[R] ⨁[ι] R := direct_sum.lof R ι (λ _:ι, R)

def std_basis (i:ι) := lof i (1:R)

@[simp] noncomputable def to_finsupp (x : ⨁[ι] R) : (ι →₀ R) :=
{ support := dfinsupp.support x,
  to_fun  := λ i, component i x,
  mem_support_to_fun := by {finish}}

def of_finsupp (f : ι →₀ R) := (finsupp.support f).sum(
    λ (i:ι), f i • @std_basis R _ ι _ i
)

-- kronecker delta on ι with values in R
@[simp] def δ (i j : ι) : R := ite (j = i) (1:R) 0

@[simp] lemma apply_eq_component (x : ⨁[ι] R) (i :ι) :
    to_finsupp x i = component i x := rfl

@[simp] lemma comp_std_basis (i j : ι) :
 (component i) (std_basis j) = @δ R _ ι _ i j :=
 begin rw δ, split_ifs with h,
{rw [h, std_basis, direct_sum.component.lof_self]},
{have H := @direct_sum.component.of R _ ι _ (λ _:ι, R) _ _ i j 1,
 simp only [eq_rec_constant] at H,
 have : (direct_sum.component R ι (λ (_x : ι), R) i) = (component i) := rfl,
 rw this at H,
 rw std_basis,
 replace this : (direct_sum.lof R ι (λ (_x : ι), R) j) = lof j := rfl,
 rw this at H,
 rw H, finish}
end

noncomputable lemma equiv_finsupp : (⨁[ι] R) ≃ₗ[R] ι →₀ R := {
    to_fun  := to_finsupp,
    add     := by {intros x y, ext1, induction x, induction y, all_goals {refl}},
    smul    := by {intros _ x, ext1, induction x, all_goals {refl}},
    inv_fun := of_finsupp,
  left_inv  := begin intro x, rw ext_iff, intro i,
        rw [of_finsupp, linear_map.map_sum (component i)],
        simp only [algebra.id.smul_eq_mul, comp_std_basis, linear_map.map_smul, δ,
                   mul_boole, finset.sum_ite_eq', finsupp.mem_support_iff, ne.def],
        split_ifs; tauto end,
  right_inv := begin intro f, ext i,
        suffices : (component i) (of_finsupp f) = f i, {tauto},
        rw [of_finsupp, linear_map.map_sum (component i)],
        simp only [mul_boole, algebra.id.smul_eq_mul, finset.sum_ite_eq', δ,
            finsupp.mem_support_iff, comp_std_basis, ne.def,
            linear_map.map_smul],
        split_ifs; finish end}

lemma is_basis_std_basis : @is_basis ι R (⨁[ι] R) std_basis _ _ _ :=
begin
rw is_basis, split,
-- linear independence
{rw linear_independent_iff', intros, rw ext_iff at a, replace a := a i,
simp only [linear_map.map_zero, comp_std_basis, smul_eq_mul, linear_map.map_sum, linear_map.map_smul, δ] at *, finish},
-- span
{rw submodule.span, simp only [Inf_eq_top, set.mem_set_of_eq] at *, intros,
ext1, split, tauto, intros hx, cases hx,
replace H : ∀ (i:ι), std_basis i ∈ a := by
        {intro, apply H, fconstructor, from i, refl},
apply direct_sum.induction_on x,
    {finish},
    {intros i r, have Hi := H i,
    suffices : lof i r ∈ a, {tauto},
    rw [← mul_one r, ← smul_eq_mul, linear_map.map_smul],
    from a.smul_mem r Hi},
    {intros y z, from a.add_mem}}
end

variables {M : Type v} [add_comm_group M] [module R M]

variables (R)
lemma lmap_of_elt.smul (m : M):
     ∀ (c x : R), (λ (r : R), r • m) (c • x) = c • (λ (r : R), r • m) x
:= begin intros r s, simp only [algebra.id.smul_eq_mul, mul_smul] at *, end
def lmap_of_elt (m : M): R →ₗ[R] M :=
    linear_map.mk (λ (r:R), r•m) (λ x y, add_smul x y m) (lmap_of_elt.smul R m)
lemma elt_of_lmap_of_elt_of_one (m : M) : m = lmap_of_elt R m (1:R) :=
begin rw lmap_of_elt, simp only [linear_map.coe_mk, one_smul] end

def lmap_of_elts (m : ι → M) : (⨁[ι] R) →ₗ[R] M :=
to_module (λ (i:ι), lmap_of_elt R (m i))

lemma needs_a_name (m : ι → M) (i : ι) :
    (lmap_of_elts R m) (std_basis i) = m i :=
begin
rw lmap_of_elts, rw std_basis, simp only [direct_sum.to_module_lof],
from (elt_of_lmap_of_elt_of_one R (m i)).symm
end

variables (M)
variables {R}
-- set_option trace.simplify.rewrite true
lemma surj_of_fg (hfg : (⊤ : submodule R M).fg) :
    ∃ (ι : Type v) [fintype ι], ∃ (π : (⨁[ι] R) →ₗ[R] M), function.surjective π  :=
begin
cases hfg with s hs,
let ι₀ : set M := ↑s, let ι  : Type v := ↥ι₀,
use ι, fconstructor, {apply_instance},
let π₀ : ι → M := λ i, i,
let π := lmap_of_elts R π₀,
fconstructor, {use π},
{let πι := π '' set.range (@std_basis R _ ι _),
 have πι' :
     πι = set.range (λ (x : (set.range (@std_basis R _ ι _))), π (x :⨁[ι] R))
    := set.image_eq_range π (set.range (@std_basis R _ ι _)),
have Rπι_eq_πRι :=
    @submodule.span_image R (⨁[ι] R) M _ _ _ _ _ (set.range std_basis) π,
replace  Rπι_eq_πRι : submodule.span R πι = submodule.map π ⊤ := by
    {rw ← (@is_basis_std_basis R _ ι _).2, exact Rπι_eq_πRι},
intro m, have : m ∈ (⊤ : submodule R M) := by {tauto}, rw ← hs at this,
 rw submodule.mem_span at this, replace this := this (submodule.span R πι),
 have foo := @submodule.subset_span R M _ _ _ πι,
 replace foo : ∀ (i∈ πι), i ∈ (submodule.span R πι) := by {tauto},
 have s_le_πι : ↑s ⊆ πι :=
 begin
    suffices : ∀ (i ∈ s), i ∈ πι, {tauto},
    intros i₀ hi₀,
    let i : ι := begin fconstructor, use i₀, tauto end,
    let πi := π (@std_basis R _ ι _ (i:ι)),
    suffices : i₀ = πi,
        {rw this,
        have baz := (@set.mem_range M (set.range (@std_basis R _ ι _)) (λ (x : ↥(set.range std_basis)), π x.val) πi).mpr,

        suffices : (∃ (y : (set.range (@std_basis R _ ι _))),
            (λ (x : (set.range (@std_basis R _ ι _))), π x.val) y = πi),
            {rw πι',apply baz, from this},
        let y := @std_basis R _ ι _ i, use y,
        rw set.mem_range, use i},
    have : πi = π₀ i := by {have := @needs_a_name R _ ι _ M _ _ π₀ i, finish},
    rw this,
    replace this : π₀ i = i := rfl,
    rw this, refl,
 end,
 have : m ∈ submodule.span R πι :=
 begin
    apply this,
    suffices : ∀ (i ∈ s), i ∈ (submodule.span R πι),
        tauto,
    replace s_le_πι : ∀ (i ∈ s), i ∈ πι := by {tauto},
    intros i hi, from foo i (s_le_πι i hi),
 end,
 --  easy to finish from here
 rw Rπι_eq_πRι at this, rw submodule.map at this, cases this with a ha,
 use a, from ha.2,
}
end

end free

[Johan Commelin]

@Sam Lichtenstein Wow, nice work. I encourage you to also look at the API for finsupp. For example, there is finsupp.single which is almost the Kronecker delta (except that it takes any scalar, instead of fixing on 1). It would be good to do the same thing here, as it is predictable.
I'll now load the code into VScode.

[Sam Lichtenstein]

I'll take a look at single tomorrow. Here is a slightly improved version of surj_of_fg removing some back-and-forth nonsense:

lemma surj_of_fg (hfg : (⊤ : submodule R M).fg) :
    ∃ (ι : Type v) [fintype ι], ∃ (π : (⨁[ι] R) →ₗ[R] M), function.surjective π  :=
begin
cases hfg with s hs,
let ι₀ : set M := ↑s, let ι  : Type v := ↥ι₀,
use ι, fconstructor, {apply_instance},
let π₀ : ι → M := λ i, i,
let π := lmap_of_elts R π₀,
fconstructor, {use π},
{let πι := π '' set.range (@std_basis R _ ι _),
 have πι' :
     πι = set.range (λ (x : (set.range (@std_basis R _ ι _))), π (x :⨁[ι] R))
    := set.image_eq_range π (set.range (@std_basis R _ ι _)),
have Rπι_eq_πRι :=
    @submodule.span_image R (⨁[ι] R) M _ _ _ _ _ (set.range std_basis) π,
replace  Rπι_eq_πRι : submodule.span R πι = submodule.map π ⊤ := by
    {rw ← (@is_basis_std_basis R _ ι _).2, exact Rπι_eq_πRι},
intro m, have : m ∈ (⊤ : submodule R M) := by {tauto}, rw ← hs at this,
 rw submodule.mem_span at this, replace this := this (submodule.span R πι),
 have foo := @submodule.subset_span R M _ _ _ πι,
 replace foo : ∀ (i∈ πι), i ∈ (submodule.span R πι) := by {tauto},
 have s_le_πι : ∀ (i ∈ s), i ∈ πι :=
 begin
    intros i₀ hi₀,
    let i : ι := begin fconstructor, use i₀, tauto end,
    let πi := π (@std_basis R _ ι _ (i:ι)),
    suffices : i₀ = πi,
        {rw this,
        have baz := (@set.mem_range M (set.range (@std_basis R _ ι _)) (λ (x : ↥(set.range std_basis)), π x.val) πi).mpr,

        suffices : (∃ (y : (set.range (@std_basis R _ ι _))),
            (λ (x : (set.range (@std_basis R _ ι _))), π x.val) y = πi),
            {rw πι',apply baz, from this},
        let y := @std_basis R _ ι _ i, use y,
        rw set.mem_range, use i},
    have : πi = π₀ i := by {have := @needs_a_name R _ ι _ M _ _ π₀ i, finish},
    rw this,
    replace this : π₀ i = i := rfl,
    rw this, refl,
 end,
 have : m ∈ submodule.span R πι := by {apply this, intros i hi,
                                       exact foo i (s_le_πι i hi)},
 -- easy to finish from here
 rw Rπι_eq_πRι at this, rw submodule.map at this, cases this with a ha,
 use a, from ha.2,
}
end

[Johan Commelin]

@Sam Lichtenstein Concerning the notation: what do you think of

notation `⨁` binders `, ` r:(scoped f, direct_sum _ f) := r

example : ⨁ i:ι, R := 0

[Johan Commelin]

That way, you generalise the notation to arbitrary direct sums.

[Johan Commelin]

It does mean that you wouldn't have explicit notation for free

[Johan Commelin]

So that's a downside

[Sam Lichtenstein]

hrm I need to think about it. I think the point of the API I made is that the non-dependent case should be simpler to work with. But I agree that it doesn't really make sense to restrict ⨁ to non-dependent direct sums!

[Johan Commelin]

API design is hard...

[Sam Lichtenstein]

If the parser can handle superscripts, there's still the idea of using $R^{\oplus \iota}$.

[Johan Commelin]

When I copy paste your code into a new file, I get errors on this line

instance free.module : module R ⨁[ι] R := direct_sum.module

It says it doesn't know about direct_sum.module

[Sam Lichtenstein]

Or more generally $M^{\oplus \iota}$ -- that should always refer toa non-dependent sum!

[Johan Commelin]

Sam Lichtenstein said:

If the parser can handle superscripts, there's still the idea of using $R^{\oplus \iota}$.

Well... we can only do unicode :sad:

[Sam Lichtenstein]

Can you use the second version I posted at 12:42?

[Sam Lichtenstein]

I switched to using a namespace and the instances are anonymous now

[Johan Commelin]

Aah.. you are using an old mathlib, I guess

[Sam Lichtenstein]

[package]
name = "pid"
version = "0.1"
lean_version = "leanprover-community/lean:3.14.0"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "cc06d538378b040fcd60c80412cf6e5cecf93ff7"}

[Sam Lichtenstein]

probably a few days old at least

[Johan Commelin]

Yup

[Johan Commelin]

Since then modules have been generalised to "semimodules" over semirings

[Johan Commelin]

So it's direct_sum.semimodule now

[Sam Lichtenstein]

anyways bed time for me. I can try to merge with the upstream changes later this week

[Johan Commelin]

Sure

[Johan Commelin]

Also, when you post several screens of code, would you please put a copy on gist.github (or some other pastebin)?

[Mario Carneiro]

Johan Commelin said:

Sam Lichtenstein said:

If the parser can handle superscripts, there's still the idea of using $R^{\oplus \iota}$.

Well... we can only do unicode :sad:

You can always use ^⨁

[Johan Commelin]

It's useful to see the code on zulip. But copy-pasting is hard

[Johan Commelin]

At least, I haven't figured out a trick to copy an entire code block from zulip. (They should offer a "copy this" link)

[Johan Commelin]

@Sam Lichtenstein Sleep well!

[Sam Lichtenstein]

https://gist.github.com/sflicht/53bdcdb1e3536e668736f7b4eb63cd79

[Mario Carneiro]

instance : module R ⨁[ι] R := direct_sum.module

The precedence here looks a little odd. It should probably be around 40, not 500

[Mario Carneiro]

(ι → (R →ₗ[R] M)) → (⨁[ι] R) →ₗ[R] M :=

The trailing precedence should also be higher than 0 so that the parentheses are not necessary here

[Johan Commelin]

@Sam Lichtenstein I've sent you an invitation for write access to non-master branches on the mathlib repo. You can put your code in a branch there. That way, others can easily take a look, and using leanproject we'll never have to worry about which version of lean or mathlib that's being used.

[Johan Commelin]

One problem with the library is that a lot of linear algebra is developed in terms of finsupp, and not direct_sum.

[Johan Commelin]

Ouch, direct_sum clearly hasn't been used a lot. There are names like direct_sum.to_module that do what a mathematician think they should do :shock:
(Instead of being some typeclass instance thingy, it's actually a linear map to a module. In mathlib parlance, that map would be called lift, blehh.)

[Scott Morrison]

A reminder also that has_finite_biproducts landed in mathlib not so long ago, so there is a uniform API for talking about direct sums available in any category. We even use ⨁ as a notation for indexed biproducts.

[Johan Commelin]

@Sam Lichtenstein Here's my first attempt:

lemma free.surj_of_fg (hfg : (⊤ : submodule R M).fg) :
    ∃ (ι : Type v) [fintype ι], ∃ (π : (⨁[ι] R) →ₗ[R] M), function.surjective π  :=
begin
  cases hfg with s hs,
  let ι := {m : M // m ∈ s},
  let π₀ : ι → M := λ i, i,
  let π := lmap_of_elts R π₀,
  refine ⟨ι, infer_instance, π, _⟩,
  intro m,
  have hm : m ∈ submodule.span R (subtype.val '' (set.univ : set ι)),
  { simp [hs] },
  rw finsupp.mem_span_iff_total at hm,
  rcases hm with ⟨l, hl, hlm⟩,
  refine ⟨free.of_finsupp l, _⟩,
  rw ← hlm,
  rw [free.of_finsupp, linear_map.map_sum],
  apply finset.sum_congr rfl,
  rintro ⟨i, hi⟩ hil,
  dsimp [π, free.std_basis, lmap_of_elts, π₀],
  delta free.to_module free.lof,
  rw [← linear_map.map_smul, direct_sum.to_module_lof],
  rw [linear_map.map_smul],
  simp [lmap_of_elt],
end

[Johan Commelin]

I also kicked out al the decidable_eq \io from the file, and added noncomputable theory to the top of the file.

[Kevin Buzzard]

One thing to be said for single rather than the mathematician's more instinctive basis defined by the delta function is that the free module is the abelian group generated by single i r but it's only the R-module generated by the basis. This sounds like a minor point but actually in the theory of derivations of multivariable polynomials this was a decisive simplification. An induction procedure of the form "check on singles and on sums" is easier to use than "check on a basis and on sums and on R-multiples" because then you have to deal with multiplying a general element of the module by an element of R, and there are times when this is much harder to deal with than multiplying a basis element by R.

[Kevin Buzzard]

In summary, single makes sure you make module elements in the simplest possible way

[Sam Lichtenstein]

there seems to be a bit of a tradeoff: using "good" API design (e.g. building linear algebra in terms of finsupp rather than direct_sum, favoring single rather than $\delta_{ij}$ , and calling the universal mapping-out property of the module co-product lift instead of to_module) actually makes the API more impenetrable for newer users like me (at least those coming from a more math rather than CS perspective)...

[Johan Commelin]

I completely agree that lift is a bad name

[Johan Commelin]

@Sam Lichtenstein On the other hand, if you have group.to_monoid and ring.to_add_group etc... as standard names for "forgetful functors" then you get caught of guard when direct_sum.to_module is something completely different.

[Johan Commelin]

I don't think developping lin.alg in terms of finsupp instead of direct_sum is "good" API design.

[Johan Commelin]

It just so happened. But certainly we need a good API for direct_sum. I was just observing that it isn't there yet.

[Sam Lichtenstein]

@Scott Morrison I can't quite tell whether you would actually recommend using the high level category-theoretic direct sum API. AFAICT, it looks like algebra/category/Group/* shows that $\mathrm{Ab}$ is a preadditive category with all colimits and finite direct sums are biproducts. (Does it actually show that $\mathrm{Ab}$ is an abelian category, or maybe this follows from the above?) But there are comments pointing out that the colimit construction used there is at least not definitionally equal to the finsupp version used for linear algebra over $\mathbf{Z}$ elsewhere in mathlib. And it seems like there is much less done for $\mathrm{Mod}_{/R}$ than for $\mathrm{Ab}$ in algebra/category/Module/*.

[Johan Commelin]

Abelian categories were added somewhere the last 10? days... so I wouldn't expect there to be very much...

[Scott Morrison]

Well, the brief version is that the category_theory/ directory remains largely disconnected from the rest of the library. There are some good reasons for this (one should use only as much category theory as one needs...). The most important one is that people have found it hard to use, in large part because of universe polymorphism issues. This has got better recently, however.

[Scott Morrison]

But I think overall we should be trying to use it more.

[Reid Barton]

I think the main reasons it is hard to use is that it has not been used, and it has not been designed with use in mind.

[Reid Barton]

At least, not the special shapes of limits stuff (which would include direct_sum). The rest is mostly fine I think.

[Patrick Massot]

I don't think "it has not been designed with use in mind"

[Scott Morrison]

I mostly got started on it because I wanted to play with automation, but then got sucked in to trying to provide things that it seemed people wanted...

[Scott Morrison]

but, as Reid says, the special shapes of limits stuff has never been particularly satisfactory.

[Patrick Massot]

But it would certainly help if people who wrote that part of the library could show us how to use it.

[Reid Barton]

I do think the special shapes of limits stuff is just really hard. In the rest of the library we just ignore this issue completely.

[Reid Barton]

e.g. I spent quite a while trying to define homeomorph.sum_prod_distrib : (α ⊕ β) × γ ≃ₜ α × γ ⊕ β × γ in terms of homeomorph.sigma_prod_distrib : ((Σ i, σ i) × β) ≃ₜ (Σ i, (σ i × β)), and eventually I just gave up and copied the proof

[Bhavik Mehta]

Patrick Massot said:

But it would certainly help if people who wrote that part of the library could show us how to use it.

Is there anything in particular you think would be helpful? Personally I found it reasonably easy to get my head around when I first tried, and it's been getting gradually better (although I agree it's not particularly nice to use)

[Scott Morrison]

(deleted)

[Scott Morrison]

In terms of using it, I hope that we've now laid good foundations for doing homological algebra, which should come quickly now.

[Scott Morrison]

Similarly with abelian categories and semisimplicity around the corner, I think it will be useful in the near future as we start doing some representation theory.

[Bhavik Mehta]

I think the thing for me is that map_cone and relatives can be pretty annoying to use, especially when related to limits of special shapes but I have no idea how one would do it better

[Patrick Massot]

Having usable homological algebra using category theory would be awesome. Of course the other big test is sheaf theory.

[Patrick Massot]

So you could try to do sheaf cohomology, and check all boxes.

[Bhavik Mehta]

Sheaf theory should be coming soon!

[Patrick Massot]

Testing the interface with the concrete world could be something like relating sheaf cohomology with a low tech definition of Cech cohomology for instance (when it makes sense).

[Sebastien Gouezel]

What I would love to see is the fact that, if $K$ and $L$ are two homeomorphic compact subsets of the sphere $S^n$, then $S^n - K$ and $S^n - L$ have the same number of connected components (which contains Jordan curve theorem as a trivial case). A.k.a. Alexander duality. I have just seen on Wikipedia that this follows from a more general theorem of completely abstract flavor https://en.wikipedia.org/wiki/Spanier%E2%80%93Whitehead_duality, for which I can't parse the statement :)

[Johan Commelin]

@Sebastien Gouezel Are your K and L homeomorphic?

[Johan Commelin]

Otherwise I don't see how to believe your claim

[Sebastien Gouezel]

Yes, obviously. That's what the original message says now :)

[Sam Lichtenstein]

is there really a non-circular proof of the Jordan curve theorem along such lines?

[Patrick Massot]

Yes

[Sam Lichtenstein]

cool

[Reid Barton]

In fact I think the Jordan curve theorem is proved in this way in HOL Light, and maybe also Isabelle

[Reid Barton]

oh, actually I see not using Alexander duality, but still using homology
https://www.mathematics.pitt.edu/hales60/pdf/Harrison-John.pdf

[Sebastien Gouezel]

The original proofs in HOL Light and Isabelle were naive proofs, without homology. It was refactored in HOL Light to use homology, but the Isabelle one is still the original one, with bare hands.

[Kevin Buzzard]

@Scott Morrison we will get there in the end. Every time I've used the category theory library it's got easier. It's still really hard to use though. About a month ago I spent over an hour trying to do a trivial-on-paper codewars category theory question and then gave up. Every single new concept (natural transformations, pushouts/pullbacks, products, general limits, concrete categories, ...) comes with its own API and for some reason I find it much harder to extract the API from the source lean files than I do with something like an algebra file written by Kenny, where I just read it and then know what I'm doing immediately. I find it hard to believe that my understanding of pushouts is somehow deficient compared to my understanding of R-algebras, but somehow I still find pushouts harder to use than R-algebras. Writing those basic docs on natural transformations etc helped me, but I feel like I need to write basic docs on all the other things too before I can use it. I don't know why this is -- genuinely. There is some measure of "hard for Kevin to work with" which I can't quantify -- I really want to believe that category theory at the level I want to use it should be completely content-free (I only ever use very basic stuff about pullbacks and Yoneda etc in reality) whereas I feel that I'm doing harder stuff with algebra, but somehow I find algebra easier to formalise, in the sense that I can do it slowly, whereas with category theory sometimes I just can't do it at all. This is most definitely not a criticism of your work! It's just a frustrated brain-dump on my part.

[Jalex Stark]

Johan Commelin said:

At least, I haven't figured out a trick to copy an entire code block from zulip. (They should offer a "copy this" link)

There's a "view source button". After I click that, I click inside of the box that the text comes in, press cmd-a. Then all of the text is highlighted and i can copy it. I'm on macOS + chrome (but i'd guess that your setup has some similar functionality)

[Kevin Buzzard]

Don't you then have to delete the ``` s?

[Jalex Stark]

yes, I suppose so. I think it's lower friction to delete one line of text than to click an external link from zulip, but I can imagine someone else feeling differently

[Johan Commelin]

@Jalex Stark Thanks, that works. (Though I would still like a little 'copy-to-clipboard' button. I guess I should start an issue over at zulip's github.)