EtaleFundamentalGroups.Purity.exists_injective_dual_scalarQuotient_of_exact
Dualizing an exact pair whose second map is scalar multiplication embeds the scalar quotient of the middle dual into the first dual.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open scoped Pointwise
variable {R A B E : Type u} [CommRing R]
variable [AddCommGroup A] [Module R A]
variable [AddCommGroup B] [Module R B]
variable [AddCommGroup E] [Module R E] [Module.Injective R E]Lean source · statement
theorem exists_injective_dual_scalarQuotient_of_exact
(δ : A →ₗ[R] B) (x : R)
(hex : Function.Exact δ (x • (LinearMap.id : B →ₗ[R] B))) :
∃ f : ((B →ₗ[R] E) ⧸ x • (⊤ : Submodule R (B →ₗ[R] E))) →ₗ[R]
(A →ₗ[R] E), Function.Injective f