## Stream: maths

### Topic: f.g. free modules

#### Kevin Buzzard (Jun 01 2020 at 11:32):

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 (Jun 01 2020 at 11:47):

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

#### Kevin Buzzard (Jun 01 2020 at 11:56):

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

#### Kevin Buzzard (Jun 01 2020 at 12:39):

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 (Jun 01 2020 at 12:41):

We could define free in terms of ι →₀ R

#### Johan Commelin (Jun 01 2020 at 12:41):

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 (Jun 01 2020 at 13:09):

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 (Jun 01 2020 at 13:14):

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 (Jun 01 2020 at 13:54):

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 (Jun 01 2020 at 13:57):

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

#### Kevin Buzzard (Jun 01 2020 at 13:59):

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 (Jun 01 2020 at 14:03):

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 (Jun 01 2020 at 14:03):

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

hey we can do that??!!

#### Kevin Buzzard (Jun 01 2020 at 14:06):

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 (Jun 01 2020 at 14:10):

@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 (Jun 01 2020 at 14:12):

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 (Jun 01 2020 at 14:17):

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

#### Reid Barton (Jun 01 2020 at 14:20):

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 (Jun 01 2020 at 14:29):

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

#### Sam Lichtenstein (Jun 01 2020 at 14:29):

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

#### Johan Commelin (Jun 01 2020 at 16:16):

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

#### Johan Commelin (Jun 01 2020 at 16:17):

It would basically be

notation \bigoplus := direct_sum


#### Johan Commelin (Jun 01 2020 at 16:20):

@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 (Jun 01 2020 at 16:30):

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

#### Johan Commelin (Jun 01 2020 at 16:35):

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

#### Johan Commelin (Jun 01 2020 at 16:35):

:fire: burn unicode to the ground :fire:

#### Johan Commelin (Jun 01 2020 at 16:35):

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

#### Johan Commelin (Jun 01 2020 at 16:36):

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

#### Reid Barton (Jun 01 2020 at 16:58):

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

#### Reid Barton (Jun 01 2020 at 16:58):

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

#### Johan Commelin (Jun 01 2020 at 16:58):

That's \slightlybiggerthannormaloplus

#### Sam Lichtenstein (Jun 01 2020 at 17:16):

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

#### Bryan Gin-ge Chen (Jun 01 2020 at 17:31):

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

#### Sam Lichtenstein (Jun 02 2020 at 03:48):

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 ι

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},
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 (Jun 02 2020 at 04:42):

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 ι

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},
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 (Jun 02 2020 at 04:49):

@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 (Jun 02 2020 at 04:50):

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 (Jun 02 2020 at 04:55):

@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 (Jun 02 2020 at 04:56):

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

#### Johan Commelin (Jun 02 2020 at 04:56):

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

#### Johan Commelin (Jun 02 2020 at 04:56):

So that's a downside

#### Sam Lichtenstein (Jun 02 2020 at 04:57):

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 (Jun 02 2020 at 04:58):

API design is hard...

#### Sam Lichtenstein (Jun 02 2020 at 04:58):

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

#### Johan Commelin (Jun 02 2020 at 04:59):

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 (Jun 02 2020 at 04:59):

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

#### Johan Commelin (Jun 02 2020 at 04:59):

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 (Jun 02 2020 at 05:00):

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

#### Sam Lichtenstein (Jun 02 2020 at 05:00):

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

#### Johan Commelin (Jun 02 2020 at 05:00):

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

#### Sam Lichtenstein (Jun 02 2020 at 05:01):

[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 (Jun 02 2020 at 05:01):

probably a few days old at least

Yup

#### Johan Commelin (Jun 02 2020 at 05:02):

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

#### Johan Commelin (Jun 02 2020 at 05:02):

So it's direct_sum.semimodule now

#### Sam Lichtenstein (Jun 02 2020 at 05:02):

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

Sure

#### Johan Commelin (Jun 02 2020 at 05:02):

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

#### Mario Carneiro (Jun 02 2020 at 05:02):

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 (Jun 02 2020 at 05:02):

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

#### Johan Commelin (Jun 02 2020 at 05:03):

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 (Jun 02 2020 at 05:03):

@Sam Lichtenstein Sleep well!

#### Sam Lichtenstein (Jun 02 2020 at 05:05):

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

#### Mario Carneiro (Jun 02 2020 at 05:11):

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

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

#### Mario Carneiro (Jun 02 2020 at 05:13):

 (ι → (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 (Jun 02 2020 at 05:16):

@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 (Jun 02 2020 at 05:23):

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

#### Johan Commelin (Jun 02 2020 at 05:27):

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 (Jun 02 2020 at 05:36):

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 (Jun 02 2020 at 05:53):

@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 (Jun 02 2020 at 05:53):

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

#### Kevin Buzzard (Jun 02 2020 at 06:34):

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 (Jun 02 2020 at 06:50):

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

#### Sam Lichtenstein (Jun 02 2020 at 12:38):

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 (Jun 02 2020 at 12:43):

I completely agree that lift is a bad name

#### Johan Commelin (Jun 02 2020 at 12:44):

@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 (Jun 02 2020 at 12:45):

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

#### Johan Commelin (Jun 02 2020 at 12:45):

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 (Jun 02 2020 at 13:41):

@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 (Jun 02 2020 at 13:49):

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

#### Scott Morrison (Jun 02 2020 at 13:50):

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 (Jun 02 2020 at 13:50):

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

#### Reid Barton (Jun 02 2020 at 13:51):

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 (Jun 02 2020 at 13:51):

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

#### Patrick Massot (Jun 02 2020 at 13:51):

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

#### Scott Morrison (Jun 02 2020 at 13:52):

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 (Jun 02 2020 at 13:52):

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

#### Patrick Massot (Jun 02 2020 at 13:52):

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

#### Reid Barton (Jun 02 2020 at 13:53):

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 (Jun 02 2020 at 13:54):

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 (Jun 02 2020 at 13:56):

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)

(deleted)

#### Scott Morrison (Jun 02 2020 at 13:58):

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 (Jun 02 2020 at 13:59):

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 (Jun 02 2020 at 14:01):

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 (Jun 02 2020 at 14:07):

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

#### Patrick Massot (Jun 02 2020 at 14:08):

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

#### Bhavik Mehta (Jun 02 2020 at 14:08):

Sheaf theory should be coming soon!

#### Patrick Massot (Jun 02 2020 at 14:09):

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 (Jun 02 2020 at 14:31):

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 (Jun 02 2020 at 14:35):

@Sebastien Gouezel Are your K and L homeomorphic?

#### Johan Commelin (Jun 02 2020 at 14:35):

Otherwise I don't see how to believe your claim

#### Sebastien Gouezel (Jun 02 2020 at 14:42):

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

#### Sam Lichtenstein (Jun 02 2020 at 14:45):

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

Yes

cool

#### Reid Barton (Jun 02 2020 at 15:17):

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

#### Reid Barton (Jun 02 2020 at 15:23):

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

#### Sebastien Gouezel (Jun 02 2020 at 15:28):

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 (Jun 02 2020 at 15:52):

@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 (Jun 03 2020 at 20:32):

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 (Jun 03 2020 at 21:02):

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

#### Jalex Stark (Jun 03 2020 at 21:26):

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 (Jun 04 2020 at 04:53):

@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.)

Last updated: May 19 2021 at 00:40 UTC