From 7453aab0b63cac2198dd56c6c2898d90283288d8 Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Tue, 21 Mar 2023 10:36:09 +0800 Subject: [PATCH 1/4] feat: port RingTheory.Flat From fa6d4df98589b23a18d12f273bc657e0c8d18815 Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Tue, 21 Mar 2023 10:36:09 +0800 Subject: [PATCH 2/4] Initial file copy from mathport --- Mathlib/RingTheory/Flat.lean | 85 ++++++++++++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 Mathlib/RingTheory/Flat.lean diff --git a/Mathlib/RingTheory/Flat.lean b/Mathlib/RingTheory/Flat.lean new file mode 100644 index 0000000000000..f3a68f5bf65e1 --- /dev/null +++ b/Mathlib/RingTheory/Flat.lean @@ -0,0 +1,85 @@ +/- +Copyright (c) 2020 Johan Commelin. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johan Commelin + +! This file was ported from Lean 3 source module ring_theory.flat +! leanprover-community/mathlib commit 62c0a4ef1441edb463095ea02a06e87f3dfe135c +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.RingTheory.Noetherian + +/-! +# Flat modules + +A module `M` over a commutative ring `R` is *flat* +if for all finitely generated ideals `I` of `R`, +the canonical map `I ⊗ M →ₗ M` is injective. + +This is equivalent to the claim that for all injective `R`-linear maps `f : M₁ → M₂` +the induced map `M₁ ⊗ M → M₂ ⊗ M` is injective. +See . +This result is not yet formalised. + +## Main declaration + +* `module.flat`: the predicate asserting that an `R`-module `M` is flat. + +## TODO + +* Show that tensoring with a flat module preserves injective morphisms. + Show that this is equivalent to be flat. + See . + To do this, it is probably a good idea to think about a suitable + categorical induction principle that should be applied to the category of `R`-modules, + and that will take care of the administrative side of the proof. +* Define flat `R`-algebras +* Define flat ring homomorphisms + - Show that the identity is flat + - Show that composition of flat morphisms is flat +* Show that flatness is stable under base change (aka extension of scalars) + For base change, it will be very useful to have a "characteristic predicate" + instead of relying on the construction `A ⊗ B`. + Indeed, such a predicate should allow us to treat both + `A[X]` and `A ⊗ R[X]` as the base change of `R[X]` to `A`. + (Similar examples exist with `fin n → R`, `R × R`, `ℤ[i] ⊗ ℝ`, etc...) +* Generalize flatness to noncommutative rings. + +-/ + + +universe u v + +namespace Module + +open Function (Injective) + +open LinearMap (lsmul) + +open TensorProduct + +/-- An `R`-module `M` is flat if for all finitely generated ideals `I` of `R`, +the canonical map `I ⊗ M →ₗ M` is injective. -/ +class Flat (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Prop where + out : ∀ ⦃I : Ideal R⦄ (hI : I.Fg), Injective (TensorProduct.lift ((lsmul R M).comp I.Subtype)) +#align module.flat Module.Flat + +namespace Flat + +open TensorProduct LinearMap _Root_.Submodule + +instance self (R : Type u) [CommRing R] : Flat R R := + ⟨by + intro I hI + rw [← Equiv.injective_comp (TensorProduct.rid R I).symm.toEquiv] + convert Subtype.coe_injective using 1 + ext x + simp only [Function.comp_apply, LinearEquiv.coe_toEquiv, rid_symm_apply, comp_apply, mul_one, + lift.tmul, subtype_apply, Algebra.id.smul_eq_mul, lsmul_apply]⟩ +#align module.flat.self Module.Flat.self + +end Flat + +end Module + From 8b1ea0a2bf8ff352645a1a3216d1f824dbf00a0b Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Tue, 21 Mar 2023 10:36:09 +0800 Subject: [PATCH 3/4] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + Mathlib/RingTheory/Flat.lean | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib.lean b/Mathlib.lean index 8e4c0bba2d23c..976f0509e71e6 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1279,6 +1279,7 @@ import Mathlib.RingTheory.Coprime.Ideal import Mathlib.RingTheory.Coprime.Lemmas import Mathlib.RingTheory.Finiteness import Mathlib.RingTheory.Fintype +import Mathlib.RingTheory.Flat import Mathlib.RingTheory.FreeRing import Mathlib.RingTheory.Ideal.Basic import Mathlib.RingTheory.Ideal.IdempotentFg diff --git a/Mathlib/RingTheory/Flat.lean b/Mathlib/RingTheory/Flat.lean index f3a68f5bf65e1..d234c5590baf9 100644 --- a/Mathlib/RingTheory/Flat.lean +++ b/Mathlib/RingTheory/Flat.lean @@ -8,7 +8,7 @@ Authors: Johan Commelin ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.RingTheory.Noetherian +import Mathlib.RingTheory.Noetherian /-! # Flat modules From 645c74e2472cb0e313eb28664214cdc6154c779d Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Tue, 21 Mar 2023 10:51:19 +0800 Subject: [PATCH 4/4] Fix errors --- Mathlib/RingTheory/Flat.lean | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/Mathlib/RingTheory/Flat.lean b/Mathlib/RingTheory/Flat.lean index d234c5590baf9..beaaf5fb3ac19 100644 --- a/Mathlib/RingTheory/Flat.lean +++ b/Mathlib/RingTheory/Flat.lean @@ -24,7 +24,7 @@ This result is not yet formalised. ## Main declaration -* `module.flat`: the predicate asserting that an `R`-module `M` is flat. +* `Module.Flat`: the predicate asserting that an `R`-module `M` is flat. ## TODO @@ -43,7 +43,7 @@ This result is not yet formalised. instead of relying on the construction `A ⊗ B`. Indeed, such a predicate should allow us to treat both `A[X]` and `A ⊗ R[X]` as the base change of `R[X]` to `A`. - (Similar examples exist with `fin n → R`, `R × R`, `ℤ[i] ⊗ ℝ`, etc...) + (Similar examples exist with `Fin n → R`, `R × R`, `ℤ[i] ⊗ ℝ`, etc...) * Generalize flatness to noncommutative rings. -/ @@ -62,24 +62,23 @@ open TensorProduct /-- An `R`-module `M` is flat if for all finitely generated ideals `I` of `R`, the canonical map `I ⊗ M →ₗ M` is injective. -/ class Flat (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Prop where - out : ∀ ⦃I : Ideal R⦄ (hI : I.Fg), Injective (TensorProduct.lift ((lsmul R M).comp I.Subtype)) + out : ∀ ⦃I : Ideal R⦄ (_ : I.Fg), Injective (TensorProduct.lift ((lsmul R M).comp I.subtype)) #align module.flat Module.Flat namespace Flat -open TensorProduct LinearMap _Root_.Submodule +open TensorProduct LinearMap Submodule instance self (R : Type u) [CommRing R] : Flat R R := ⟨by - intro I hI + intro I _ rw [← Equiv.injective_comp (TensorProduct.rid R I).symm.toEquiv] convert Subtype.coe_injective using 1 ext x simp only [Function.comp_apply, LinearEquiv.coe_toEquiv, rid_symm_apply, comp_apply, mul_one, - lift.tmul, subtype_apply, Algebra.id.smul_eq_mul, lsmul_apply]⟩ + lift.tmul, Submodule.subtype_apply, Algebra.id.smul_eq_mul, lsmul_apply]⟩ #align module.flat.self Module.Flat.self end Flat end Module -