Documentation

ModuleLocalProperties.MissingLemmas.LocalizaedIsTensorProduct

def wfw {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (S : Submonoid R) :
Equations
noncomputable def IsBaseChange.lift' {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {M' : Type u_5} [AddCommGroup M'] [Module R M'] [Module S M'] [IsScalarTower R S M'] {fm : M →ₗ[R] M'} (hm : IsBaseChange S fm) {N' : Type u_6} [AddCommGroup N'] [Module R N'] [Module S N'] [IsScalarTower R S N'] (fn : N →ₗ[R] N') (f : M →ₗ[R] N) :
M' →ₗ[S] N'
Equations
  • hm.lift' fn f = hm.lift (fn ∘ₗ f)
noncomputable def LinearMap.isBaseChangeHom {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] {M : Type u_3} (N : Type u_4) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {M' : Type u_5} [AddCommGroup M'] [Module R M'] [Module S M'] [IsScalarTower R S M'] {fm : M →ₗ[R] M'} (hm : IsBaseChange S fm) (N' : Type u_6) [AddCommGroup N'] [Module R N'] [Module S N'] [IsScalarTower R S N'] (fn : N →ₗ[R] N') :
(M →ₗ[R] N) →ₗ[R] M' →ₗ[S] N'
Equations
noncomputable def IsBaseChange.lift_bilinMap {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {M' : Type u_5} [AddCommGroup M'] [Module R M'] [Module S M'] [IsScalarTower R S M'] {fm : M →ₗ[R] M'} (hm : IsBaseChange S fm) {N' : Type u_6} [AddCommGroup N'] [Module R N'] [Module S N'] [IsScalarTower R S N'] {fn : N →ₗ[R] N'} (hn : IsBaseChange S fn) {P : Type u_7} [AddCommGroup P] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) {P' : Type u_8} [AddCommGroup P'] [Module R P'] [Module S P'] [IsScalarTower R S P'] (g : P →ₗ[R] P') :
M' →ₗ[S] N' →ₗ[S] P'
Equations
theorem IsBaseChange.iff_isTensorProduct_lift_bilinMap {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {M' : Type u_5} [AddCommGroup M'] [Module R M'] [Module S M'] [IsScalarTower R S M'] {fm : M →ₗ[R] M'} (hm : IsBaseChange S fm) {N' : Type u_6} [AddCommGroup N'] [Module R N'] [Module S N'] [IsScalarTower R S N'] {fn : N →ₗ[R] N'} (hn : IsBaseChange S fn) {P : Type u_7} [AddCommGroup P] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) {P' : Type u_8} [AddCommGroup P'] [Module R P'] [Module S P'] [IsScalarTower R S P'] (g : P →ₗ[R] P') :
IsBaseChange S g IsTensorProduct (hm.lift_bilinMap hn f g)