free.lean

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_πι : ∀ (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

end free