EtaleFundamentalGroups.Purity.injective_linearMap_of_flat
The linear dual of a flat module with values in an injective module is injective. The extension is obtained by tensoring, extending, and currying; no injectivity assumption on the dual is needed.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Purity
universe u
open scoped TensorProduct
variable {R : Type u} [CommRing R]Lean source · full declaration
theorem injective_linearMap_of_flat
(F E : Type u) [AddCommGroup F] [Module R F] [Module.Flat R F]
[AddCommGroup E] [Module R E] [Module.Injective R E] :
Module.Injective R (F →ₗ[R] E) where
out X Y _ _ _ _ f hf g := by
have hft : Function.Injective (f.rTensor F) :=
Module.Flat.rTensor_preserves_injective_linearMap f hf
obtain ⟨h, hh⟩ := Module.Injective.out (f.rTensor F) hft (TensorProduct.lift g)
refine ⟨TensorProduct.curry h, ?_⟩
intro x
ext z
simpa only [TensorProduct.curry_apply, LinearMap.rTensor_tmul,
TensorProduct.lift.tmul] using hh (x ⊗ₜ[R] z)