Base change properties for modules of linear maps

• IsBaseChange.linearMapRight: If M is finite free 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 is finite free 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 is finite free 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_5} [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

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_5} [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

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_5} [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_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [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.

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_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [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)

@[simp]

theorem IsBaseChange.linearMapLeftRightHom_comp_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_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [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) (m : M) : ((j.linearMapLeftRightHom β) f) (α m) = β (f m)

@[simp]

theorem IsBaseChange.linearMapLeftRightHom_comp {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_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [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) : ↑R ((j.linearMapLeftRightHom β) f) ∘ₗ α = β ∘ₗ f

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_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [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_5} [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.

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_5} [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.endHom_comp_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_5} [AddCommMonoid P] [Module R P] [Module S P] [IsScalarTower R S P] {α : M →ₗ[R] P} (j : IsBaseChange S α) (f : M →ₗ[R] M) (m : M) : (j.endHom f) (α m) = α (f m)

theorem IsBaseChange.endHom_comp {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_5} [AddCommMonoid P] [Module R P] [Module S P] [IsScalarTower R S P] {α : M →ₗ[R] P} (j : IsBaseChange S α) (f : M →ₗ[R] M) : ↑R (j.endHom f) ∘ₗ α = α ∘ₗ f

theorem IsBaseChange.endHom_one {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_5} [AddCommMonoid P] [Module R P] [Module S P] [IsScalarTower R S P] {α : M →ₗ[R] P} (j : IsBaseChange S α) : j.endHom 1 = 1

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_5} [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.linearMapLeftRightHom_toMatrix {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_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [AddCommMonoid Q] [Module R Q] [Module S P] [IsScalarTower R S P] [Module S Q] [IsScalarTower R S Q] {α : M →ₗ[R] P} {β : N →ₗ[R] Q} (ibcM : IsBaseChange S α) (ibcN : IsBaseChange S β) {ι : Type u_7} {θ : Type u_8} [DecidableEq ι] [Fintype ι] [Finite θ] (b : Module.Basis ι R M) (c : Module.Basis θ R N) (f : M →ₗ[R] N) : (LinearMap.toMatrix (basis b ibcM) (basis c ibcN)) ((ibcM.linearMapLeftRightHom β) f) = ((LinearMap.toMatrix b c) f).map ⇑(algebraMap R S)

theorem IsBaseChange.endHom_toMatrix {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_5} [AddCommMonoid P] [Module R P] [Module S P] [IsScalarTower R S P] {α : M →ₗ[R] P} (ibcM : IsBaseChange S α) {ι : Type u_7} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) (f : M →ₗ[R] M) : (LinearMap.toMatrix (basis b ibcM) (basis b ibcM)) (ibcM.endHom f) = ((LinearMap.toMatrix b b) f).map ⇑(algebraMap R S)

theorem IsBaseChange.det_endHom {R : Type u_6} [CommRing R] (S : Type u_7) [CommRing S] [Algebra R S] (M : Type u_8) [AddCommGroup M] [Module R M] {P : Type u_9} [AddCommGroup 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 α) (f : M →ₗ[R] M) : LinearMap.det (j.endHom f) = (algebraMap R S) (LinearMap.det f)