Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- /-
- 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
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement