Created
November 3, 2020 16:55
-
-
Save rmfedorov/6dae5d559bd0dafd9f87300bf1e537ad to your computer and use it in GitHub Desktop.
Code for flat modules
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/- | |
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment