def
wfw
{R : Type u_1}
[CommRing R]
(I : Ideal R)
(M : Type u_2)
[AddCommGroup M]
[Module R M]
(S : Submonoid R)
:
↥(Ideal.map (algebraMap R (Localization S)) I) →ₗ[R] LocalizedModule S M →ₗ[R] LocalizedModule S (TensorProduct R (↥I) M)
Equations
- wfw I M S = sorryAx (↥(Ideal.map (algebraMap R (Localization S)) I) →ₗ[R] LocalizedModule S M →ₗ[R] LocalizedModule S (TensorProduct R (↥I) M))
def
efwef
{R : Type u_1}
(M : Type u_2)
(N : Type u_3)
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(S : Submonoid R)
:
LocalizedModule S M →ₗ[R] LocalizedModule S N →ₗ[R] LocalizedModule S (TensorProduct R M N)
Equations
- efwef M N S = sorryAx (LocalizedModule S M →ₗ[R] LocalizedModule S N →ₗ[R] LocalizedModule S (TensorProduct R M N))
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)
:
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')
:
Equations
- LinearMap.isBaseChangeHom S N hm N' fn = { toFun := fun (f : M →ₗ[R] N) => hm.lift' fn f, map_add' := ⋯, map_smul' := ⋯ }
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')
:
Equations
- hm.lift_bilinMap hn f g = hm.lift' (LinearMap.isBaseChangeHom S P hn P' g) f
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)