/-
Copyright (c) 2020 Roman Fedorov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Roman Fedorov
Flat modules over rings are defined. It is proved that a module is flat over itself and that the tensor product of 
flat modules is flat. 
-/
import algebra.module
import linear_algebra.tensor_product
import data.equiv.basic
open tensor_product module linear_map
open_locale tensor_product

/-!
# Flat modules over commutative rings.

In this file we introduce flat modules over commutative rings. It is proved that 

## Main definitions and results

- `is_flat` : The definition of a flat module
- `flat_over_self` : A ring is flat as a module over itself,
- `tensor_product_is_flat` : The tensor product of flat modules is flat
- `non_zero_divisor_of_flat` : A non-zero divisor in a ring remains a non-zero divisor 
    in any flat module

## Auxiliary results

- A function whose composition with an invertible function is injective, is itself
  injective
- The left and right unit isomorphisms for tensor product are functorial
- The associator for tensor product is functorial in the third variable 
-/

/- TODO: Direct sum of any family of flat modules is flat. Thus a free module is flat.
 The problem is that it should be done for infinite direct sums but they are not yet defined. -/


universe u 

variables {R : Type u} [comm_ring R]
variables {M : Type u} {N : Type u} {P : Type u}
variables [add_comm_group M] [add_comm_group N] [add_comm_group P]
variables [module R M] [module R N] [module R P]

/-! If a functions becomes injective after composing with an invertible function, then 
it was injective from the very beginning. Probably belongs to data.equiv.basic -/
section auxiliary_result_about_functions
universe v
variables {α β γ  : Type v}

lemma inv_comp (g : α ≃ β) (x : β) : g (g.inv_fun x) = x := by simp
lemma inv_comp' (g : α ≃ β) (x : α) : g.inv_fun (g x) = x := by simp

lemma injective_of_comp_bijective (f : β → γ) (g : α ≃ β) :
  function.injective (f ∘ g) → function.injective f := 
assume hinj : function.injective (f ∘ g),
assume x y : β,
assume heq : f x = f y,
let h:=g.inv_fun in
have (f ∘ g) (h x) = (f ∘ g) (h y), from calc
  (f ∘ g) (h x) = f (g ( h x)) : by simp 
  ...           = f x          : by rw [inv_comp g x]
  ...           = f y          : heq
  ... = f (g ( h y))           : by rw [inv_comp g y]
  ... = (f ∘ g) (h y)          : by simp,
have h x = h y, from hinj this,
show x = y, from calc
  x = g (h x)   : (inv_comp g x).symm
  ... = g (h y) : by rw [this]
  ... = y       : (inv_comp g y) 

lemma injective_of_comp_bijective' (f : α → β) (g : β ≃ γ) :
  function.injective (g ∘ f) → function.injective f :=
assume hinj : function.injective (g ∘ f),
assume x y : α,
assume heq : f x = f y,
let h:=g.inv_fun in 
have (g ∘ f) x = (g ∘ f) y, from calc
  (g ∘ f) x = g (f x) : by simp
  ... = g (f y)       : by rw[heq]
  ... = (g ∘ f) y     : by simp,
show x = y, from hinj this

end auxiliary_result_about_functions

section functoriality_of_tensor_product 

/-- The isomorphism R ⊗[R] M ≃ₗ M is functorial in M. 
Probably belongs to linear_algebra.tensor_product. -/
theorem tensor_product_lid_functorial (f : M →ₗ[R] N) :
  (tensor_product.lid R N : R ⊗[R] N ≃ₗ N) ∘ (map id f : (R ⊗[R] M) →ₗ[R] (R ⊗[R] N)) =
  f ∘ (tensor_product.lid R M : R ⊗[R] M ≃ₗ M) := 
let g : R ⊗[R] M ≃ₗ M := tensor_product.lid R M in 
let h : R ⊗[R] N ≃ₗ N := tensor_product.lid R N in 
let ft : (R ⊗[R] M) →ₗ[R] (R ⊗[R] N) := map id f in 
have h_compose : comp h.to_linear_map ft = comp f g.to_linear_map, by
{
  apply tensor_product.ext,
  intros r m,
  repeat{rw [comp_apply]},
  exact calc
  h.to_linear_map (ft (r ⊗ₜ[R] m)) = (h.to_linear_map) ((linear_map.id r) ⊗ₜ[R] (f m)) : 
    by rw map_tmul 
  ... = (tensor_product.lid R N) (r ⊗ₜ[R] (f m)) : rfl
  ... = r • f m                                  :  by rw [tensor_product.lid_tmul (f m) r]
  ... = f (r • m)                                : (f.map_smul r m).symm
  ... = f ((tensor_product.lid R M) (r ⊗ₜ[R] m)) : by rw [tensor_product.lid_tmul m r]
  ... = f (g.to_linear_map (r ⊗ₜ[R] m))          : rfl
},
by
{
  apply funext,
  exact (ext_iff.1 h_compose)
}

/-- The isomorphism M ⊗[R] R ≃ₗ M is functorial in M. 
Probably belongs to linear_algebra.tensor_product. -/
theorem tensor_product_rid_functorial (f : M →ₗ[R] N) :
  (tensor_product.rid R N : N ⊗[R] R ≃ₗ N) ∘ (map f id : (M ⊗[R] R) →ₗ[R] (N ⊗[R] R)) =
  f ∘ (tensor_product.rid R M : M ⊗[R] R ≃ₗ M) :=
let g : M ⊗[R] R ≃ₗ M := tensor_product.rid R M in 
let h : N ⊗[R] R ≃ₗ N := tensor_product.rid R N in 
let ft : (M ⊗[R] R) →ₗ[R] (N ⊗[R] R) := map f  id in 
have h_compose : (comp h.to_linear_map ft = comp f g.to_linear_map), by
{
  apply tensor_product.ext,
  intros m r,
  repeat{rw [comp_apply]},
  exact calc
  h.to_linear_map (ft (m ⊗ₜ[R] r)) = (h.to_linear_map) ((f m) ⊗ₜ[R] (linear_map.id r)) : 
    by rw map_tmul
    ... = (tensor_product.rid R N) ((f m) ⊗ₜ[R] r) : rfl
    ... = r • f m                                  : by rw [tensor_product.rid_tmul (f m) r]
    ... = f (r • m)                                : (f.map_smul r m).symm
    ... = f ((tensor_product.rid R M) (m ⊗ₜ[R] r)) : by rw [tensor_product.rid_tmul m r]
    ... = f (g.to_linear_map (m ⊗ₜ[R] r))          : rfl
},
by
{
  apply funext,
  exact (ext_iff.1 h_compose)
}

/-- The associator for tensor product is functorial in the third argument. 
Probably belongs to linear_algebra.tensor_product.-/
variable (P)

lemma assoc_functorial (Q: Type u) [add_comm_group Q] [module R Q] (f : M →ₗ[R] N) :
let ft : (Q ⊗[R] M) →ₗ[R] (Q ⊗[R] N) := map  id f in
let ftt : (P ⊗[R] (Q ⊗[R] M)) →ₗ[R](P ⊗[R] (Q ⊗[R] N)) := map  id ft in
let ftt': ((P ⊗[R] Q) ⊗[R] M) →ₗ[R]((P ⊗[R] Q) ⊗[R] N) := map id f in 
let α := tensor_product.assoc R P Q M in let β := tensor_product.assoc R P Q N in
  comp ftt α.to_linear_map  = comp β.to_linear_map ftt' := 
let ft : (Q ⊗[R] M) →ₗ[R] (Q ⊗[R] N) := map  id f in
let ftt : (P ⊗[R] (Q ⊗[R] M)) →ₗ[R](P ⊗[R] (Q ⊗[R] N)) := map id ft in
let ftt': ((P ⊗[R] Q) ⊗[R] M) →ₗ[R]((P ⊗[R] Q) ⊗[R] N) := map  id f in 
let α := tensor_product.assoc R P Q M in let β := tensor_product.assoc R P Q N in
  ext_threefold (assume (p : P) (q : Q) (m : M),
  have heq₁  : (comp ftt α.to_linear_map) ((p ⊗ₜ q) ⊗ₜ m) = (p ⊗ₜ (q ⊗ₜ f m)), from calc
    (comp ftt α.to_linear_map) ((p ⊗ₜ q) ⊗ₜ m) = ftt (α.to_linear_map ((p ⊗ₜ q) ⊗ₜ m)) : 
      comp_apply _ _ _ 
    ... = ftt (p ⊗ₜ (q ⊗ₜ m)) : by refl
    ... = (linear_map.id p) ⊗ₜ ft (q ⊗ₜ m) : map_tmul _ _ _ _
    ... = p ⊗ₜ ft (q ⊗ₜ m)                 : by rw[ id_apply] 
    ... = p ⊗ₜ ((linear_map.id q) ⊗ₜ f m)  : by rw [map_tmul _ _ _ _]
    ... = p ⊗ₜ (q ⊗ₜ f m)                  : by rw[ id_apply],
  have heq₂ : (comp β.to_linear_map ftt') ((p ⊗ₜ q) ⊗ₜ m) = (p ⊗ₜ (q ⊗ₜ f m)), from calc
    (comp β.to_linear_map ftt') ((p ⊗ₜ q) ⊗ₜ m) = β.to_linear_map (ftt' ((p ⊗ₜ q) ⊗ₜ m)) :
        comp_apply _ _ _ 
    ... = β.to_linear_map ((linear_map.id (p ⊗ₜ q)) ⊗ₜ f m) : by rw[map_tmul _ _ _ _]
    ... = β.to_linear_map ((p ⊗ₜ q) ⊗ₜ f m)                 : by rw[ id_apply]
    ... = (p ⊗ₜ (q ⊗ₜ f m))                                 : by refl,
  heq₁.trans heq₂)

end functoriality_of_tensor_product

/-- Scalar multiplication gives a linear map. Probably belongs to linear_algebra.tensor_product.-/
def linear_map_smul (P : Type u) [add_comm_group P] [module R P] (r : R) : P →ₗ[R] P :=
{to_fun := (λ (x : P), r • x), 
map_add' := (is_linear_map.is_linear_map_smul r).map_add,
map_smul' := (is_linear_map.is_linear_map_smul r).map_smul}

section flat_modules

def injective_after_tensoring (P : Type u) [add_comm_group P] [module R P] (f : M →ₗ[R] N): Prop :=
let ft : (P ⊗[R] M) →ₗ[R] (P ⊗[R] N) := map  id f in function.injective ft

/-- The definition of a flat module-/
def is_flat (P : Type u) [add_comm_group P] [module R P] : Prop :=
  ∀ (M : Type u ) (N : Type u) [add_comm_group M] [add_comm_group N],
by exactI ∀ [module R M] [module R N],
by exactI ∀ (f : M →ₗ[R] N), (function.injective f) → (injective_after_tensoring P f)

lemma remains_injective_tensor_self (f : M →ₗ[R] N) : 
  function.injective f → injective_after_tensoring R f :=
assume h_inj : function.injective f,
let g : R ⊗[R] M ≃ₗ M := tensor_product.lid R M in 
let h : R ⊗[R] N ≃ₗ N := tensor_product.lid R N in 
let ft : (R ⊗[R] M) →ₗ[R] (R ⊗[R] N) := map  id f in 
have function.injective (f ∘ g), 
from function.injective.comp h_inj $ equiv.injective $ linear_equiv.to_equiv g,
have function.injective (h ∘ ft), from eq.subst (tensor_product_lid_functorial f).symm this,
show function.injective ft, from function.injective.of_comp this
     
/-- A module is flat over itself -/
theorem flat_over_self : @is_flat R _ R _ _  :=
λ (M : Type u) (N : Type u) [add_comm_group M] [add_comm_group N], 
by exactI λ [module R M] [module R N],
by exactI λ (f : M →ₗ[R] N), (remains_injective_tensor_self f)

theorem tensor_product_is_flat (P Q : Type u) [add_comm_group P] [add_comm_group Q] 
  [module R P] [module R Q] (FLP : @is_flat R _ P _ _) (FLQ : @is_flat R _ Q _ _) :
  @is_flat R _ (P ⊗[R] Q) _ _:= 
λ (M : Type u) (N : Type u) [add_comm_group M] [add_comm_group N], 
by exactI λ [module R M] [module R N],
by exactI λ f : M →ₗ[R] N, 
assume inj : function.injective f, 
let ft : (Q ⊗[R] M) →ₗ[R] (Q ⊗[R] N) := map id f in
have injt : function.injective ft, from FLQ M N f inj,
let ftt : (P ⊗[R] (Q ⊗[R] M)) →ₗ[R](P ⊗[R] (Q ⊗[R] N)) := map id ft in
have injt : function.injective ftt, from FLP (Q ⊗[R] M) (Q ⊗[R] N) ft injt, 
let ftt': ((P ⊗[R] Q) ⊗[R] M) →ₗ[R]((P ⊗[R] Q) ⊗[R] N) := map id f in 
let h₁ := tensor_product.assoc R P Q M in let h₂ := tensor_product.assoc R P Q N in
have Comm : comp ftt (h₁.to_linear_map) = comp (h₂.to_linear_map) ftt', 
from assoc_functorial P Q f,
have Comm': ftt ∘ h₁ = h₂ ∘ ftt', by {funext, exact
(calc
  (ftt ∘ h₁) x = ftt (h₁ x) : rfl
  ... =  (comp ftt (h₁.to_linear_map)) x :  by {rw[comp_apply], refl}
  ... =  (comp (h₂.to_linear_map) ftt') x : by rw[Comm]
  ... = h₂ (ftt' x) :                       by {rw[comp_apply], refl}
  ... = (h₂ ∘ ftt') x :                     rfl),
},
have function.injective (ftt ∘ h₁), 
from function.injective.comp injt $ equiv.injective $ linear_equiv.to_equiv h₁,
have function.injective (h₂  ∘ ftt'), from Comm' ▸ this,
show function.injective ftt', 
from injective_of_comp_bijective' ftt' (linear_equiv.to_equiv h₂) this

/-- A non-zero divisor in R remains a non-zero divisor on any flat R-module-/
theorem non_zero_divisor_of_flat (P : Type u) [add_comm_group P] [module R P] 
  (FL : @is_flat R _ P _ _) (r : R) (non_div : function.injective (λ (x : R), r * x)) : 
  function.injective (λ (x : P), r • x) := 
let f : P →ₗ[R] P := linear_map_smul P r  in
let g : R →ₗ[R] R := linear_map_smul R r in
let gt : (P ⊗[R] R) →ₗ[R] (P ⊗[R] R) := map  id g in
have h_inj : function.injective gt, from FL R R g non_div, 
let h : P ⊗[R] R ≃ₗ P := tensor_product.rid R P in 
have gt = map f id, by
{
  apply tensor_product.ext,
  intros p r',
  repeat{rw [comp_apply]},
  exact calc
    gt (p ⊗ₜ[R] r')= (linear_map.id p) ⊗ₜ[R] (g r') : by rw map_tmul
    ... = p ⊗ₜ[R] (r * r')                          : rfl
    ... = (r • p) ⊗ₜ[R] r'                          : (smul_tmul _ _ _).symm
    ... = (f p) ⊗ₜ[R] ( linear_map.id r')           : rfl
    ... = (map f linear_map.id) (p ⊗ₜ[R] r')        : by rw map_tmul
},
have Comm : h ∘ gt = f ∘ h, by rw [this, tensor_product_rid_functorial f],
have function.injective (h ∘ gt), 
from function.injective.comp (equiv.injective (linear_equiv.to_equiv h)) h_inj,
have function.injective (f ∘ h), from Comm ▸ this,
show function.injective f, from injective_of_comp_bijective f (linear_equiv.to_equiv h) this

end flat_modules