noncomputable def LocalizedModule.BilinearMap {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommSemiring R] (S : Submonoid R) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) : LocalizedModule S M →ₗ[Localization S] LocalizedModule S N →ₗ[Localization S] LocalizedModule S P

Equations

• LocalizedModule.BilinearMap S f = LocalizedModule.LocalizedMapLift S ∘ₗ (LocalizedModule.mapfromlift S) f

theorem LocalizedModule.BilinearMap_mk {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommSemiring R] (S : Submonoid R) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) (s : ↥S) (t : ↥S) : ((LocalizedModule.BilinearMap S f) (LocalizedModule.mk m s)) (LocalizedModule.mk n t) = LocalizedModule.mk ((f m) n) (s * t)

noncomputable def LocalizedModule.TensorProductBilinearMap {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : LocalizedModule S M →ₗ[Localization S] LocalizedModule S N →ₗ[Localization S] LocalizedModule S (TensorProduct R M N)

Equations

• LocalizedModule.TensorProductBilinearMap S M N = LocalizedModule.BilinearMap S (TensorProduct.mk R M N)

theorem LocalizedModule.TensorProductBilinearMap_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (m : M) (n : N) (s : ↥S) (t : ↥S) : ((LocalizedModule.TensorProductBilinearMap S M N) (LocalizedModule.mk m s)) (LocalizedModule.mk n t) = LocalizedModule.mk (m ⊗ₜ[R] n) (s * t)

noncomputable def LocalizedModule.TensorProductMap {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : TensorProduct (Localization S) (LocalizedModule S M) (LocalizedModule S N) →ₗ[Localization S] LocalizedModule S (TensorProduct R M N)

Equations

• LocalizedModule.TensorProductMap S M N = TensorProduct.lift (LocalizedModule.TensorProductBilinearMap S M N)

theorem LocalizedModule.TensorProductMap_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (m : M) (n : N) (s : ↥S) (t : ↥S) : (LocalizedModule.TensorProductMap S M N) (LocalizedModule.mk m s ⊗ₜ[Localization S] LocalizedModule.mk n t) = LocalizedModule.mk (m ⊗ₜ[R] n) (s * t)

noncomputable def LocalizedModule.InvTensorProductBilinearMap {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : M →ₗ[R] N →ₗ[R] TensorProduct (Localization S) (LocalizedModule S M) (LocalizedModule S N)

Equations

• One or more equations did not get rendered due to their size.

theorem LocalizedModule.InvTensorProductBilinearMap_apply {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (m : M) (n : N) : ((LocalizedModule.InvTensorProductBilinearMap S M N) m) n = LocalizedModule.mk m 1 ⊗ₜ[Localization S] LocalizedModule.mk n 1

noncomputable def LocalizedModule.InvTensorProductMap' {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : TensorProduct R M N →ₗ[R] TensorProduct (Localization S) (LocalizedModule S M) (LocalizedModule S N)

Equations

• LocalizedModule.InvTensorProductMap' S M N = TensorProduct.lift (LocalizedModule.InvTensorProductBilinearMap S M N)

theorem LocalizedModule.InvTensorProductMap'_apply {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (m : M) (n : N) : (LocalizedModule.InvTensorProductMap' S M N) (m ⊗ₜ[R] n) = LocalizedModule.mk m 1 ⊗ₜ[Localization S] LocalizedModule.mk n 1

noncomputable def LocalizedModule.InvTensorProductMap {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : LocalizedModule S (TensorProduct R M N) →ₗ[Localization S] TensorProduct (Localization S) (LocalizedModule S M) (LocalizedModule S N)

Equations

• LocalizedModule.InvTensorProductMap S M N = LocalizedModule.LiftOnLocalizationModule S (LocalizedModule.InvTensorProductMap' S M N)

theorem LocalizedModule.InvTensorProductMap_apply {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (m : M) (n : N) (s : ↥S) : (LocalizedModule.InvTensorProductMap S M N) (LocalizedModule.mk (m ⊗ₜ[R] n) s) = Localization.mk 1 s • LocalizedModule.mk m 1 ⊗ₜ[Localization S] LocalizedModule.mk n 1

theorem LocalizedModule.InvTensorProductMap_apply' {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (m : M) (n : N) (s : ↥S) (t : ↥S) : (LocalizedModule.InvTensorProductMap S M N) (LocalizedModule.mk (m ⊗ₜ[R] n) (s * t)) = LocalizedModule.mk m s ⊗ₜ[Localization S] LocalizedModule.mk n t

theorem LocalizedModule.TensorProductMap_rightInv {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : LocalizedModule.TensorProductMap S M N ∘ₗ LocalizedModule.InvTensorProductMap S M N = LinearMap.id

theorem LocalizedModule.TensorProductMap_leftInv {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : LocalizedModule.InvTensorProductMap S M N ∘ₗ LocalizedModule.TensorProductMap S M N = LinearMap.id

noncomputable def LocalizedModule.TensorProductEquiv {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : TensorProduct (Localization S) (LocalizedModule S M) (LocalizedModule S N) ≃ₗ[Localization S] LocalizedModule S (TensorProduct R M N)

Equations

• LocalizedModule.TensorProductEquiv S M N = LinearEquiv.ofLinear (LocalizedModule.TensorProductMap S M N) (LocalizedModule.InvTensorProductMap S M N) ⋯ ⋯

theorem LocalizedModule.TensorProductEquiv_apply {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (m : M) (n : N) (s : ↥S) (t : ↥S) : (LocalizedModule.TensorProductEquiv S M N) (LocalizedModule.mk m s ⊗ₜ[Localization S] LocalizedModule.mk n t) = LocalizedModule.mk (m ⊗ₜ[R] n) (s * t)

theorem LocalizedModule.TensorProductEquiv_symm_apply {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) (N : Type u_3) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (m : M) (n : N) (s : ↥S) : (LocalizedModule.TensorProductEquiv S M N).symm (LocalizedModule.mk (m ⊗ₜ[R] n) s) = Localization.mk 1 s • LocalizedModule.mk m 1 ⊗ₜ[Localization S] LocalizedModule.mk n 1