Base change properties for modules of linear maps

• IsBaseChange.linearMapRight: If M has a finite basis and P is a base change of N to S, then M →ₗ[R] P is a base change of M →ₗ[R] N to S.

• IsBaseChange.linearMapLeftRight: If M has a finite basis and P is a base change of M to S, if Q is a base change of N to S, then P →ₗ[S] Q is a base change of M →ₗ[R] N to S.

• IsBaseChange.end: If M has a finite basis and P is a base change of M to S, then P →ₗ[S] P is a base change of M →ₗ[R] M to S.

def IsBaseChange.linearMapRightBaseChangeHom {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (M : Type u_3) [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] {P : Type u_6} [AddCommMonoid P] [Module R P] [Module S P] [IsScalarTower R S P] (ε : N →ₗ[R] P) : TensorProduct R S (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P

The base change homomorphism underlying IsBaseChange.linearMapRight

Equations

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

noncomputable def IsBaseChange.linearMapRightBaseChangeEquiv {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (M : Type u_3) [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] {P : Type u_6} [AddCommMonoid P] [Module R P] [Module S P] [IsScalarTower R S P] [Module.Free R M] [Module.Finite R M] {ε : N →ₗ[R] P} (ibc : IsBaseChange S ε) : TensorProduct R S (M →ₗ[R] N) ≃ₗ[S] M →ₗ[R] P

The base change isomorphism funderlying IsBaseChange.linearMapRight

Equations

• IsBaseChange.linearMapRightBaseChangeEquiv M ibc = LinearEquiv.ofBijective (IsBaseChange.linearMapRightBaseChangeHom S M ε) ⋯

theorem IsBaseChange.linearMapRight {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (M : Type u_3) [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] {P : Type u_6} [AddCommMonoid P] [Module R P] [Module S P] [IsScalarTower R S P] [Module.Free R M] [Module.Finite R M] {ε : N →ₗ[R] P} (ibc : IsBaseChange S ε) : IsBaseChange S (LinearMap.compRight R ε)

If M has a finite basis and P is a base change of N to S, then M →ₗ[R] P is a base change of M →ₗ[R] N to S.

noncomputable def IsBaseChange.linearMapLeftRightHom {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {M : Type u_3} [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] {P : Type u_6} [AddCommMonoid P] [Module R P] {Q : Type u_7} [AddCommMonoid Q] [Module R Q] [Module S P] [IsScalarTower R S P] [Module S Q] [IsScalarTower R S Q] {α : M →ₗ[R] P} (j : IsBaseChange S α) (β : N →ₗ[R] Q) : (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q

The base change map for linear maps with source a free finite module.

Equations

• j.linearMapLeftRightHom β = ↑R ((LinearMap.llcomp S P (TensorProduct R S M) Q).flip ↑j.equiv.symm) ∘ₗ ↑R ↑(LinearMap.liftBaseChangeEquiv S) ∘ₗ LinearMap.compRight R β

theorem IsBaseChange.linearMapLeftRightHom_apply {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {M : Type u_3} [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] {P : Type u_6} [AddCommMonoid P] [Module R P] {Q : Type u_7} [AddCommMonoid Q] [Module R Q] [Module S P] [IsScalarTower R S P] [Module S Q] [IsScalarTower R S Q] {α : M →ₗ[R] P} (j : IsBaseChange S α) (β : N →ₗ[R] Q) (f : M →ₗ[R] N) (p : P) : ((j.linearMapLeftRightHom β) f) p = ((LinearMap.liftBaseChangeEquiv S) (β ∘ₗ f)) (j.equiv.symm p)

theorem IsBaseChange.linearMapLeftRight {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {M : Type u_3} [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] {P : Type u_6} [AddCommMonoid P] [Module R P] {Q : Type u_7} [AddCommMonoid Q] [Module R Q] [Module S P] [IsScalarTower R S P] [Module S Q] [IsScalarTower R S Q] [Module.Free R M] [Module.Finite R M] {α : M →ₗ[R] P} (j : IsBaseChange S α) {β : N →ₗ[R] Q} (k : IsBaseChange S β) : IsBaseChange S (j.linearMapLeftRightHom β)

noncomputable def IsBaseChange.endHom {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {M : Type u_3} [AddCommMonoid M] [Module R M] {P : Type u_6} [AddCommMonoid P] [Module R P] [Module S P] [IsScalarTower R S P] {α : M →ₗ[R] P} (j : IsBaseChange S α) : (M →ₗ[R] M) →ₗ[R] P →ₗ[S] P

The base change map for endomorphisms of a free finite module.

Equations

• j.endHom = ↑R ((LinearMap.llcomp S P (TensorProduct R S M) P).flip ↑j.equiv.symm) ∘ₗ ↑R ↑(LinearMap.liftBaseChangeEquiv S) ∘ₗ LinearMap.compRight R α

theorem IsBaseChange.endHom_apply {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {M : Type u_3} [AddCommMonoid M] [Module R M] {P : Type u_6} [AddCommMonoid P] [Module R P] [Module S P] [IsScalarTower R S P] {α : M →ₗ[R] P} (j : IsBaseChange S α) (f : M →ₗ[R] M) (p : P) : (j.endHom f) p = ((LinearMap.liftBaseChangeEquiv S) (α ∘ₗ f)) (j.equiv.symm p)

theorem IsBaseChange.end {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {M : Type u_3} [AddCommMonoid M] [Module R M] {P : Type u_6} [AddCommMonoid P] [Module R P] [Module S P] [IsScalarTower R S P] [Module.Free R M] [Module.Finite R M] {α : M →ₗ[R] P} (j : IsBaseChange S α) : IsBaseChange S j.endHom

theorem IsBaseChange.« end » {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {M : Type u_3} [AddCommMonoid M] [Module R M] {P : Type u_6} [AddCommMonoid P] [Module R P] [Module S P] [IsScalarTower R S P] [Module.Free R M] [Module.Finite R M] {α : M →ₗ[R] P} (j : IsBaseChange S α) : IsBaseChange S j.endHom