The characteristic predicate of tensor product #

Main definitions #

IsTensorProduct: A predicate on f : M₁ →ₗ[R] M₂ →ₗ[R] M expressing that f realizes M as the tensor product of M₁ ⊗[R] M₂. This is defined by requiring the lift M₁ ⊗[R] M₂ → M to be bijective.
IsBaseChange: A predicate on an R-algebra S and a map f : M →ₗ[R] N with N being an S-module, expressing that f realizes N as the base change of M along R → S.
Algebra.IsPushout: A predicate on the following diagram of scalar towers
```
  R  →  S
  ↓     ↓
  R' →  S'
```
asserting that is a pushout diagram (i.e. S' = S ⊗[R] R')

Main results #

TensorProduct.isBaseChange: S ⊗[R] M is the base change of M along R → S.

def IsTensorProduct {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] (f : M₁ →ₗ[R] M₂ →ₗ[R] M) :

Prop

Given a bilinear map f : M₁ →ₗ[R] M₂ →ₗ[R] M, IsTensorProduct f means that M is the tensor product of M₁ and M₂ via f. This is defined by requiring the lift M₁ ⊗[R] M₂ → M to be bijective.

Equations

IsTensorProduct f = Function.Bijective ⇑(TensorProduct.lift f)

Instances For

source

theorem TensorProduct.isTensorProduct (R : Type u_1) [CommSemiring R] (M : Type u_4) [AddCommMonoid M] [Module R M] (N : Type u_8) [AddCommMonoid N] [Module R N] :

IsTensorProduct (mk R M N)

source

noncomputable def IsTensorProduct.equiv {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) :

TensorProduct R M₁ M₂ ≃ₗ[R] M

If M is the tensor product of M₁ and M₂, it is linearly equivalent to M₁ ⊗[R] M₂.

Equations

h.equiv = LinearEquiv.ofBijective (TensorProduct.lift f) h

Instances For

source

@[simp]

theorem IsTensorProduct.equiv_apply {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) (a✝ : TensorProduct R M₁ M₂) :

h.equiv a✝ = (TensorProduct.lift f) a✝

source

@[simp]

theorem IsTensorProduct.equiv_toLinearMap {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) :

↑h.equiv = TensorProduct.lift f

source

@[simp]

theorem IsTensorProduct.equiv_symm_apply {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) (x₁ : M₁) (x₂ : M₂) :

h.equiv.symm ((f x₁) x₂) = x₁ ⊗ₜ[R] x₂

source

noncomputable def IsTensorProduct.lift {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} {M' : Type u_5} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [AddCommMonoid M'] [Module R M₁] [Module R M₂] [Module R M] [Module R M'] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) (f' : M₁ →ₗ[R] M₂ →ₗ[R] M') :

M →ₗ[R] M'

If M is the tensor product of M₁ and M₂, we may lift a bilinear map M₁ →ₗ[R] M₂ →ₗ[R] M' to a M →ₗ[R] M'.

Equations

h.lift f' = TensorProduct.lift f' ∘ₗ ↑h.equiv.symm

Instances For

source

theorem IsTensorProduct.lift_eq {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} {M' : Type u_5} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [AddCommMonoid M'] [Module R M₁] [Module R M₂] [Module R M] [Module R M'] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) (f' : M₁ →ₗ[R] M₂ →ₗ[R] M') (x₁ : M₁) (x₂ : M₂) :

(h.lift f') ((f x₁) x₂) = (f' x₁) x₂

source

noncomputable def IsTensorProduct.map {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N] [Module R N₁] [Module R N₂] [Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) :

M →ₗ[R] N

The tensor product of a pair of linear maps between modules.

Equations

hf.map hg i₁ i₂ = ↑hg.equiv ∘ₗ TensorProduct.map i₁ i₂ ∘ₗ ↑hf.equiv.symm

Instances For

source

@[simp]

theorem IsTensorProduct.map_eq {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N] [Module R N₁] [Module R N₂] [Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (x₁ : M₁) (x₂ : M₂) :

(hf.map hg i₁ i₂) ((f x₁) x₂) = (g (i₁ x₁)) (i₂ x₂)

source

theorem IsTensorProduct.inductionOn {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) {motive : M → Prop} (m : M) (zero : motive 0) (tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)) (add : ∀ (x y : M), motive x → motive y → motive (x + y)) :

motive m

source

theorem IsTensorProduct.of_equiv {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (e : TensorProduct R M₁ M₂ ≃ₗ[R] M) (he : ∀ (x : M₁) (y : M₂), e (x ⊗ₜ[R] y) = (f x) y) :

IsTensorProduct f

source

theorem IsTensorProduct.map_comp {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N] [Module R N₁] [Module R N₂] [Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} {P₁ : Type u_9} {P₂ : Type u_10} {P : Type u_11} [AddCommMonoid P₁] [AddCommMonoid P₂] [AddCommMonoid P] [Module R P₁] [Module R P₂] [Module R P] {p : P₁ →ₗ[R] P₂ →ₗ[R] P} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (hp : IsTensorProduct p) (i₁ : N₁ →ₗ[R] P₁) (j₁ : M₁ →ₗ[R] N₁) (i₂ : N₂ →ₗ[R] P₂) (j₂ : M₂ →ₗ[R] N₂) :

hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂) = hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂

source

theorem IsTensorProduct.map_map {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N] [Module R N₁] [Module R N₂] [Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} {P₁ : Type u_9} {P₂ : Type u_10} {P : Type u_11} [AddCommMonoid P₁] [AddCommMonoid P₂] [AddCommMonoid P] [Module R P₁] [Module R P₂] [Module R P] {p : P₁ →ₗ[R] P₂ →ₗ[R] P} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (hp : IsTensorProduct p) (i₁ : N₁ →ₗ[R] P₁) (j₁ : M₁ →ₗ[R] N₁) (i₂ : N₂ →ₗ[R] P₂) (j₂ : M₂ →ₗ[R] N₂) (x : M) :

(hg.map hp i₁ i₂) ((hf.map hg j₁ j₂) x) = (hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂)) x

source

@[simp]

theorem IsTensorProduct.map_id {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f) :

hf.map hf LinearMap.id LinearMap.id = LinearMap.id

source

@[simp]

theorem IsTensorProduct.map_one {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f) :

hf.map hf 1 1 = 1

source

theorem IsTensorProduct.map_mul {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f) (i₁ i₂ : M₁ →ₗ[R] M₁) (j₁ j₂ : M₂ →ₗ[R] M₂) :

hf.map hf (i₁ * i₂) (j₁ * j₂) = hf.map hf i₁ j₁ * hf.map hf i₂ j₂

source

theorem IsTensorProduct.map_pow {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f) (i : M₁ →ₗ[R] M₁) (j : M₂ →ₗ[R] M₂) (n : ℕ) :

hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n)

source

def IsBaseChange {R : Type u_1} {M : Type v₁} {N : Type v₂} (S : Type v₃) [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) :

Prop

Given an R-algebra S and an R-module M, an S-module N together with a map f : M →ₗ[R] N is the base change of M to S if the map S × M → N, (s, m) ↦ s • f m is the tensor product.

Equations

IsBaseChange S f = IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f))

Instances For

source

noncomputable def IsBaseChange.lift {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] [Module R Q] [IsScalarTower R S Q] (g : M →ₗ[R] Q) :

N →ₗ[S] Q

Suppose f : M →ₗ[R] N is the base change of M along R → S. Then any R-linear map from M to an S-module factors through f.

Equations

h.lift g = { toAddHom := (IsTensorProduct.lift h (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g))).toAddHom, map_smul' := ⋯ }

Instances For

source

theorem IsBaseChange.lift_eq {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] [Module R Q] [IsScalarTower R S Q] (g : M →ₗ[R] Q) (x : M) :

(h.lift g) (f x) = g x

source

theorem IsBaseChange.lift_comp {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] [Module R Q] [IsScalarTower R S Q] (g : M →ₗ[R] Q) :

↑R (h.lift g) ∘ₗ f = g

source

theorem IsBaseChange.inductionOn {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) (x : N) (motive : N → Prop) (zero : motive 0) (tmul : ∀ (m : M), motive (f m)) (smul : ∀ (s : S) (n : N), motive n → motive (s • n)) (add : ∀ (n₁ n₂ : N), motive n₁ → motive n₂ → motive (n₁ + n₂)) :

motive x

source

theorem IsBaseChange.algHom_ext {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] (g₁ g₂ : N →ₗ[S] Q) (e : ∀ (x : M), g₁ (f x) = g₂ (f x)) :

g₁ = g₂

source

theorem IsBaseChange.algHom_ext' {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] [Module R Q] [IsScalarTower R S Q] (g₁ g₂ : N →ₗ[S] Q) (e : ↑R g₁ ∘ₗ f = ↑R g₂ ∘ₗ f) :

g₁ = g₂

source

theorem TensorProduct.isBaseChange (R : Type u_1) (M : Type v₁) (S : Type v₃) [AddCommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] :

IsBaseChange S ((mk R S M) 1)

source

noncomputable def IsBaseChange.equiv {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) :

TensorProduct R S M ≃ₗ[S] N

The base change of M along R → S is linearly equivalent to S ⊗[R] M.

Equations

h.equiv = { toAddHom := (↑(IsTensorProduct.equiv h)).toAddHom, map_smul' := ⋯, invFun := (IsTensorProduct.equiv h).invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

theorem IsBaseChange.equiv_tmul {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) (s : S) (m : M) :

h.equiv (s ⊗ₜ[R] m) = s • f m

source

theorem IsBaseChange.equiv_symm_apply {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) (m : M) :

h.equiv.symm (f m) = 1 ⊗ₜ[R] m

source

theorem IsBaseChange.of_equiv {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (e : TensorProduct R S M ≃ₗ[S] N) (he : ∀ (x : M), e (1 ⊗ₜ[R] x) = f x) :

IsBaseChange S f

source

theorem IsBaseChange.linearMap (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] :

IsBaseChange S (Algebra.linearMap R S)

source

theorem isBaseChange_tensorProduct_map {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {P : Type u_2} [AddCommMonoid P] [Module R P] (A : Type u_4) [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Module S M] [IsScalarTower R S M] [Module A N] [IsScalarTower S A N] [IsScalarTower R A N] {f : M →ₗ[S] N} (hf : IsBaseChange A f) :

IsBaseChange A (TensorProduct.AlgebraTensorModule.map f LinearMap.id)

If N is the base change of M to A, then N ⊗[R] P is the base change of M ⊗[R] P to A. This is simply the isomorphism A ⊗[S] (M ⊗[R] P) ≃ₗ[A] (A ⊗[S] M) ⊗[R] P.

source

theorem IsBaseChange.of_lift_unique {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) (h : ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q] [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g' : N →ₗ[S] Q, ↑R g' ∘ₗ f = g) :

IsBaseChange S f

source

theorem IsBaseChange.iff_lift_unique {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} :

IsBaseChange S f ↔ ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q] [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g' : N →ₗ[S] Q, ↑R g' ∘ₗ f = g

source

theorem IsBaseChange.ofEquiv {R : Type u_1} {M : Type v₁} {N : Type v₂} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [Module R M] [Module R N] (e : M ≃ₗ[R] N) :

IsBaseChange R ↑e

source

theorem IsBaseChange.comp {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {T : Type u_4} {O : Type u_5} [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [AddCommMonoid O] [Module R O] [Module S O] [Module T O] [IsScalarTower S T O] [IsScalarTower R S O] [IsScalarTower R T O] {f : M →ₗ[R] N} (hf : IsBaseChange S f) {g : N →ₗ[S] O} (hg : IsBaseChange T g) :

IsBaseChange T (↑R g ∘ₗ f)

source

theorem IsBaseChange.of_comp {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {T : Type u_4} {O : Type u_5} [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [AddCommMonoid O] [Module R O] [Module S O] [Module T O] [IsScalarTower S T O] [IsScalarTower R S O] [IsScalarTower R T O] {f : M →ₗ[R] N} (hf : IsBaseChange S f) {h : N →ₗ[S] O} (hc : IsBaseChange T (↑R h ∘ₗ f)) :

IsBaseChange T h

If N is the base change of M to S and O the base change of M to T, then O is the base change of N to T.

source

theorem IsBaseChange.comp_iff {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {T : Type u_4} {O : Type u_5} [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [AddCommMonoid O] [Module R O] [Module S O] [Module T O] [IsScalarTower S T O] [IsScalarTower R S O] [IsScalarTower R T O] {f : M →ₗ[R] N} (hf : IsBaseChange S f) {h : N →ₗ[S] O} :

IsBaseChange T (↑R h ∘ₗ f) ↔ IsBaseChange T h

If N is the base change M to S, then O is the base change of M to T if and only if O is the base change of N to T.

source

noncomputable def IsBaseChange.tensorEquiv {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (hf : IsBaseChange S f) (P : Type u_6) [AddCommGroup P] [Module R P] [Module S P] [IsScalarTower R S P] :

TensorProduct S P N ≃ₗ[S] TensorProduct R P M

Let R be a commutative ring, S be an R-algebra, M be an R-module, P be an S module, N be the base change of M to S, then P ⊗[S] N is isomorphic to P ⊗[R] M as S-modules.

Equations

hf.tensorEquiv P = (LinearEquiv.lTensor P hf.equiv.symm).trans (TensorProduct.AlgebraTensorModule.cancelBaseChange R S S P M)

Instances For

source

theorem IsBaseChange.map_id_lsmul_eq_lsmul_algebraMap {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (hf : IsBaseChange S f) (x : R) :

IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x) = ↑R ((LinearMap.lsmul S N) ((algebraMap R S) x))

source

class Algebra.IsPushout (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (R' : Type u_6) (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] :

Prop

A type-class stating that the following diagram of scalar towers

R  →  S
↓     ↓
R' →  S'

is a pushout diagram (i.e. S' = S ⊗[R] R')

out : IsBaseChange S (IsScalarTower.toAlgHom R R' S').toLinearMap

Instances

source

theorem Algebra.isPushout_iff (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (R' : Type u_6) (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] :

IsPushout R S R' S' ↔ IsBaseChange S (IsScalarTower.toAlgHom R R' S').toLinearMap

source

noncomputable def Algebra.IsPushout.equiv (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (R' : Type u_6) (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : IsPushout R S R' S'] :

TensorProduct R S R' ≃ₐ[S] S'

The isomorphism S' ≃ S ⊗[R] R given Algebra.IsPushout R S R' S'.

Equations

Algebra.IsPushout.equiv R S R' S' = { toFun := (↑⋯.equiv).toFun, invFun := ⋯.equiv.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source

theorem Algebra.IsPushout.equiv_tmul (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (R' : Type u_6) (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : IsPushout R S R' S'] (a : S) (b : R') :

(equiv R S R' S') (a ⊗ₜ[R] b) = (algebraMap S S') a * (algebraMap R' S') b

source

theorem Algebra.IsPushout.equiv_symm_algebraMap_left (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (R' : Type u_6) (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsPushout R S R' S'] (a : S) :

(equiv R S R' S').symm ((algebraMap S S') a) = a ⊗ₜ[R] 1

source

theorem Algebra.IsPushout.equiv_symm_algebraMap_right (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (R' : Type u_6) (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsPushout R S R' S'] (a : R') :

(equiv R S R' S').symm ((algebraMap R' S') a) = 1 ⊗ₜ[R] a

source

theorem Algebra.IsPushout.symm {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} {S' : Type u_7} [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (h : IsPushout R S R' S') :

IsPushout R R' S S'

source

theorem Algebra.IsPushout.comm (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (R' : Type u_6) (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] :

IsPushout R S R' S' ↔ IsPushout R R' S S'

source

instance instIsPushout (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] :

Algebra.IsPushout R R S S

source

instance instIsPushout_1 (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] :

Algebra.IsPushout R S R S

source

instance TensorProduct.isPushout {R : Type u_8} {S : Type u_9} {T : Type u_10} [CommSemiring R] [CommSemiring S] [CommSemiring T] [Algebra R S] [Algebra R T] :

Algebra.IsPushout R S T (TensorProduct R S T)

source

instance TensorProduct.isPushout' {R : Type u_8} {S : Type u_9} {T : Type u_10} [CommSemiring R] [CommSemiring S] [CommSemiring T] [Algebra R S] [Algebra R T] :

Algebra.IsPushout R T S (TensorProduct R S T)

source

noncomputable def Algebra.pushoutDesc {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [H : IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (hf : ∀ (x : S) (y : R'), f x * g y = g y * f x) :

S' →ₐ[R] A

If S' = S ⊗[R] R', then any pair of R-algebra homomorphisms f : S → A and g : R' → A such that f x and g y commutes for all x, y descends to a (unique) homomorphism S' → A.

Equations

Algebra.pushoutDesc S' f g hf = (Algebra.TensorProduct.lift f g hf).comp (AlgHom.restrictScalars R ↑(Algebra.IsPushout.equiv R S R' S').symm)

Instances For

source

theorem Algebra.pushoutDesc_apply {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [H : IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (hf : ∀ (x : S) (y : R'), f x * g y = g y * f x) (a✝ : S') :

(pushoutDesc S' f g hf) a✝ = (TensorProduct.lift f g hf) ((IsPushout.equiv R S R' S').symm a✝)

source

@[simp]

theorem Algebra.pushoutDesc_left {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H : ∀ (x : S) (y : R'), f x * g y = g y * f x) (x : S) :

(pushoutDesc S' f g H) ((algebraMap S S') x) = f x

source

theorem Algebra.lift_algHom_comp_left {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H : ∀ (x : S) (y : R'), f x * g y = g y * f x) :

(pushoutDesc S' f g H).comp (IsScalarTower.toAlgHom R S S') = f

source

@[simp]

theorem Algebra.pushoutDesc_right {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H : ∀ (x : S) (y : R'), f x * g y = g y * f x) (x : R') :

(pushoutDesc S' f g H) ((algebraMap R' S') x) = g x

source

theorem Algebra.lift_algHom_comp_right {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H : ∀ (x : S) (y : R'), f x * g y = g y * f x) :

(pushoutDesc S' f g H).comp (IsScalarTower.toAlgHom R R' S') = g

source

theorem Algebra.IsPushout.algHom_ext {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [H : IsPushout R S R' S'] {A : Type u_8} [Semiring A] [Algebra R A] {f g : S' →ₐ[R] A} (h₁ : f.comp (IsScalarTower.toAlgHom R R' S') = g.comp (IsScalarTower.toAlgHom R R' S')) (h₂ : f.comp (IsScalarTower.toAlgHom R S S') = g.comp (IsScalarTower.toAlgHom R S S')) :

f = g

source

theorem Algebra.IsPushout.comp_iff (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] {T : Type u_4} [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (R' : Type u_6) (S' : Type u_7) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] {T' : Type u_8} [CommSemiring T'] [Algebra R T'] [Algebra S' T'] [Algebra S T'] [Algebra T T'] [Algebra R' T'] [IsScalarTower R T T'] [IsScalarTower S T T'] [IsScalarTower S S' T'] [IsScalarTower R R' T'] [IsScalarTower R S' T'] [IsScalarTower R' S' T'] [IsPushout R S R' S'] :

IsPushout R T R' T' ↔ IsPushout S T S' T'

Let the following be a commutative diagram of rings

  R  →  S  →  T
  ↓     ↓     ↓
  R' →  S' →  T'

where the left-hand square is a pushout. Then the following are equivalent:

the big rectangle is a pushout.
the right-hand square is a pushout.

Note that this is essentially the isomorphism T ⊗[S] (S ⊗[R] R') ≃ₐ[T] T ⊗[R] R'.

source

theorem Algebra.IsPushout.of_equiv {R : Type u_1} {S : Type v₃} [CommSemiring R] [CommSemiring S] [Algebra R S] {R' : Type u_6} {S' : Type u_7} [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : IsPushout R R' S S'] {T : Type u_8} [CommSemiring T] [Algebra R' T] [Algebra S T] [Algebra R T] [IsScalarTower R S T] [IsScalarTower R R' T] (e : S' ≃ₐ[R'] T) (he : e.toRingEquiv.toRingHom.comp (algebraMap S S') = algebraMap S T) :

IsPushout R R' S T

source

noncomputable def Algebra.IsPushout.cancelBaseChangeAux (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Type u_8) (B : Type u_9) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [IsPushout R S A B] (M : Type u_10) [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] :

TensorProduct A B M ≃ₗ[R] TensorProduct R S M

(Implementation) If B = S ⊗[R] A, this is the canonical R-isomorphism: B ⊗[A] M ≃ₗ[S] S ⊗[R] M. See IsPushout.cancelBaseChange for the S-linear version.

Equations

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

Instances For

source

@[simp]

theorem Algebra.IsPushout.cancelBaseChangeAux_symm_tmul (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Type u_8) (B : Type u_9) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [IsPushout R S A B] (M : Type u_10) [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] (s : S) (m : M) :

(cancelBaseChangeAux R S A B M).symm (s ⊗ₜ[R] m) = (algebraMap S B) s ⊗ₜ[A] m

source

noncomputable def Algebra.IsPushout.cancelBaseChange (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Type u_8) (B : Type u_9) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [IsPushout R S A B] (M : Type u_10) [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] :

TensorProduct A B M ≃ₗ[S] TensorProduct R S M

If B = S ⊗[R] A, this is the canonical S-isomorphism: B ⊗[A] M ≃ₗ[S] S ⊗[R] M. This is the cancelling on the left version of TensorProduct.AlgebraTensorModule.cancelBaseChange.

Equations

Algebra.IsPushout.cancelBaseChange R S A B M = ((↑(Algebra.IsPushout.cancelBaseChangeAux R S A B M).symm).toLinearEquiv ⋯).symm

Instances For

source

@[simp]

theorem Algebra.IsPushout.cancelBaseChange_tmul (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Type u_8) (B : Type u_9) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [IsPushout R S A B] (M : Type u_10) [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] (m : M) :

(cancelBaseChange R S A B M) (1 ⊗ₜ[A] m) = 1 ⊗ₜ[R] m

source

@[simp]

theorem Algebra.IsPushout.cancelBaseChange_symm_tmul (R : Type u_1) (S : Type v₃) [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Type u_8) (B : Type u_9) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [IsPushout R S A B] (M : Type u_10) [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] (s : S) (m : M) :

(cancelBaseChange R S A B M).symm (s ⊗ₜ[R] m) = (algebraMap S B) s ⊗ₜ[A] m

Documentation

Mathlib.RingTheory.IsTensorProduct

The characteristic predicate of tensor product #

Main definitions #

Main results #