EtaleFundamentalGroups.tensorProduct_linearMap_ext_of_one_tmul
An S-linear map between scalar extensions is determined by its values on the canonical generators 1 ⊗ m.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w w'
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]
variable {N : Type w'} [AddCommGroup N] [Module R N]Lean source · statement
theorem tensorProduct_linearMap_ext_of_one_tmul
{F G : (S ⊗[R] M) →ₗ[S] (S ⊗[R] N)}
(h : ∀ m : M, F (1 ⊗ₜ[R] m) = G (1 ⊗ₜ[R] m)) :
F = G