Module.Flat.iff_rTensor_injective'
theorem Module.Flat.iff_rTensor_injective' :
∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
Module.Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))
This theorem states that an `R`-module `M` is considered flat if and only if for all ideals `I` of `R`, the tensor product of the inclusion function `I → R` and the identity function `M → M` is injective. In other words, if we take any ideal `I` from a commutative ring `R`, and map it to `R` through an inclusion map, then tensor this map with the identity map on `M`, the resulting map will always map distinct elements of `I` to distinct elements of `R ⊗ M` if and only if `M` is a flat `R`-module. The theorem also references `iff_rTensor_injective` for the case where `I` is restricted to finitely generated ideals.
More concisely: A commutative `R`-module `M` is flat if and only if for all ideals `I` of `R`, the tensor product of the inclusion map `I → R` and the identity map `M → M` is an injection.
|
Module.Flat.of_retract
theorem Module.Flat.of_retract :
∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Type w)
[inst_3 : AddCommGroup N] [inst_4 : Module R N] [f : Module.Flat R M] (i : N →ₗ[R] M) (r : M →ₗ[R] N),
r ∘ₗ i = LinearMap.id → Module.Flat R N
The theorem `Module.Flat.of_retract` states that if `M` is a flat `R`-module and there exist linear maps `i` from `N` to `M` and `r` from `M` to `N` such that their composition `r ∘ i` is the identity map, then `N` is also a flat `R`-module. In the context of module theory in abstract algebra, a module is considered "flat" if the tensor product preserves exact sequences. Hence, this theorem is about the preservation of the flat property under certain conditions.
More concisely: If `M` is a flat `R`-module and there exists an `R`-linear retract pair `(i : N → M), (r : M → N)` such that `r ∘ i = id_N`, then `N` is a flat `R`-module.
|
Module.Flat.of_linearEquiv
theorem Module.Flat.of_linearEquiv :
∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Type w)
[inst_3 : AddCommGroup N] [inst_4 : Module R N] [f : Module.Flat R M], (N ≃ₗ[R] M) → Module.Flat R N
This theorem states that if we have a module `M` over a commutative ring `R` that is flat, and another module `N` over the same ring `R` that is linearly equivalent to `M`, then `N` is also a flat module over `R`. In other words, flatness is preserved under linear equivalence in the context of modules over a commutative ring.
More concisely: If `M` is a flat module over a commutative ring `R` and `N` is linearly equivalent to `M`, then `N` is a flat module over `R`.
|
Module.Flat.of_projective_surjective
theorem Module.Flat.of_projective_surjective :
∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (ι : Type w)
[inst_3 : Module.Projective R M] (p : (ι →₀ R) →ₗ[R] M), Function.Surjective ⇑p → Module.Flat R M
The theorem states that for any commutative ring `R` and any module `M` over `R`, if `M` is a projective module and there exists a surjective linear map `p` from the free `R`-module on a discrete type `ι` to `M`, then `M` is a flat module over `R`.
In mathematical terms, this theorem asserts that if a module is projective and there is a surjection from a free module (indexed by a discrete set) onto it, then the module is flat. This theorem is part of the theory of commutative algebra, particularly the study of properties of modules over rings.
More concisely: If `M` is a projective module over a commutative ring `R` with a surjective homomorphism from a free `R`-module to `M`, then `M` is a flat module.
|
Module.Flat.iff_rTensor_injective
theorem Module.Flat.iff_rTensor_injective :
∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))
An `R`-module `M` is defined as flat if and only if for any finitely generated ideal `I` of `R`, the tensor product of the inclusion mapping from `I` to `R` and the identity mapping from `M` to `M` is an injective function. Here, an injective function is one where different inputs yield different outputs, and a finitely generated ideal is an ideal that can be generated by a finite set. The function `LinearMap.rTensor M (Submodule.subtype I)` represents the tensor product of the inclusion and identity mappings, and `Function.Injective` checks for injectiveness. The theorem extends to all ideals `I` as mentioned in `iff_rTensor_injective'`.
More concisely: An `R`-module `M` is flat if and only if for every finitely generated ideal `I` of `R`, the tensor product of the inclusion mapping from `I` to `R` and the identity mapping from `M` to `M` is an injective linear map.
|