Base change along flat modules preserves equalizers #
We show that base change along flat modules (resp. algebras) preserves kernels and equalizers.
theorem
Module.Flat.ker_lTensor_eq
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f : N →ₗ[R] P)
[Flat R M]
:
LinearMap.ker ((TensorProduct.AlgebraTensorModule.lTensor S M) f) = LinearMap.range ((TensorProduct.AlgebraTensorModule.lTensor S M) (LinearMap.ker f).subtype)
theorem
Module.Flat.eqLocus_lTensor_eq
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f g : N →ₗ[R] P)
[Flat R M]
:
LinearMap.eqLocus ((TensorProduct.AlgebraTensorModule.lTensor S M) f)
((TensorProduct.AlgebraTensorModule.lTensor S M) g) = LinearMap.range ((TensorProduct.AlgebraTensorModule.lTensor S M) (LinearMap.eqLocus f g).subtype)
def
LinearMap.tensorEqLocusBil
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f g : N →ₗ[R] P)
:
M →ₗ[S] ↥(eqLocus f g) →ₗ[R] ↥(eqLocus ((TensorProduct.AlgebraTensorModule.lTensor S M) f) ((TensorProduct.AlgebraTensorModule.lTensor S M) g))
The bilinear map corresponding to LinearMap.tensorEqLocus.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LinearMap.tensorKerBil
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f : N →ₗ[R] P)
:
The bilinear map corresponding to LinearMap.tensorKer.
Equations
- LinearMap.tensorKerBil S M f = { toFun := fun (m : M) => { toFun := fun (a : ↥(LinearMap.ker f)) => ⟨m ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
Instances For
def
LinearMap.tensorEqLocus
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f g : N →ₗ[R] P)
:
TensorProduct R M ↥(eqLocus f g) →ₗ[S] ↥(eqLocus ((TensorProduct.AlgebraTensorModule.lTensor S M) f) ((TensorProduct.AlgebraTensorModule.lTensor S M) g))
The canonical map M ⊗[R] eq(f, g) →ₗ[R] eq(𝟙 ⊗ f, 𝟙 ⊗ g).
Equations
Instances For
def
LinearMap.tensorKer
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f : N →ₗ[R] P)
:
TensorProduct R M ↥(ker f) →ₗ[S] ↥(ker ((TensorProduct.AlgebraTensorModule.lTensor S M) f))
The canonical map M ⊗[R] ker f →ₗ[R] ker (𝟙 ⊗ f).
Equations
Instances For
@[simp]
theorem
LinearMap.tensorKer_tmul
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f : N →ₗ[R] P)
(m : M)
(x : ↥(ker f))
:
@[simp]
theorem
LinearMap.tensorKer_coe
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f : N →ₗ[R] P)
(x : TensorProduct R M ↥(ker f))
:
@[simp]
theorem
LinearMap.tensorEqLocus_tmul
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f g : N →ₗ[R] P)
(m : M)
(x : ↥(eqLocus f g))
:
@[simp]
theorem
LinearMap.tensorEqLocus_coe
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f g : N →ₗ[R] P)
(x : TensorProduct R M ↥(eqLocus f g))
:
↑((tensorEqLocus S M f g) x) = (lTensor M (eqLocus f g).subtype) x
def
LinearMap.tensorKerEquiv
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f : N →ₗ[R] P)
[Module.Flat R M]
:
TensorProduct R M ↥(ker f) ≃ₗ[S] ↥(ker ((TensorProduct.AlgebraTensorModule.lTensor S M) f))
If M is R-flat, the canonical map M ⊗[R] ker f →ₗ[R] ker (𝟙 ⊗ f) is an isomorphism.
Equations
- LinearMap.tensorKerEquiv S M f = LinearEquiv.ofLinear (LinearMap.tensorKer S M f) (LinearMap.tensorKerInv✝ S M f) ⋯ ⋯
Instances For
@[simp]
theorem
LinearMap.tensorKerEquiv_apply
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f : N →ₗ[R] P)
[Module.Flat R M]
(x : TensorProduct R M ↥(ker f))
:
(tensorKerEquiv S M f) x = (tensorKer S M f) x
@[simp]
theorem
LinearMap.lTensor_ker_subtype_tensorKerEquiv_symm
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f : N →ₗ[R] P)
[Module.Flat R M]
(x : ↥(ker ((TensorProduct.AlgebraTensorModule.lTensor S M) f)))
:
(lTensor M (ker f).subtype) ((tensorKerEquiv S M f).symm x) = ↑x
def
LinearMap.tensorEqLocusEquiv
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f g : N →ₗ[R] P)
[Module.Flat R M]
:
TensorProduct R M ↥(eqLocus f g) ≃ₗ[S] ↥(eqLocus ((TensorProduct.AlgebraTensorModule.lTensor S M) f) ((TensorProduct.AlgebraTensorModule.lTensor S M) g))
If M is R-flat, the canonical map M ⊗[R] eq(f, g) →ₗ[S] eq (𝟙 ⊗ f, 𝟙 ⊗ g) is an
isomorphism.
Equations
- LinearMap.tensorEqLocusEquiv S M f g = LinearEquiv.ofLinear (LinearMap.tensorEqLocus S M f g) (LinearMap.tensorEqLocusInv✝ S M f g) ⋯ ⋯
Instances For
@[simp]
theorem
LinearMap.tensorEqLocusEquiv_apply
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f g : N →ₗ[R] P)
[Module.Flat R M]
(x : TensorProduct R M ↥(eqLocus f g))
:
(tensorEqLocusEquiv S M f g) x = (tensorEqLocus S M f g) x
@[simp]
theorem
LinearMap.lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
{P : Type u_5}
[AddCommGroup N]
[AddCommGroup P]
[Module R N]
[Module R P]
(f g : N →ₗ[R] P)
[Module.Flat R M]
(x : ↥(eqLocus ((TensorProduct.AlgebraTensorModule.lTensor S M) f) ((TensorProduct.AlgebraTensorModule.lTensor S M) g)))
:
(lTensor M (eqLocus f g).subtype) ((tensorEqLocusEquiv S M f g).symm x) = ↑x
def
AlgHom.tensorEqualizer
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(T : Type u_3)
[CommRing T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
{A : Type u_4}
{B : Type u_5}
[CommRing A]
[CommRing B]
[Algebra R A]
[Algebra R B]
(f g : A →ₐ[R] B)
:
TensorProduct R T ↥(equalizer f g) →ₐ[S] ↥(equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f) (Algebra.TensorProduct.map (AlgHom.id S T) g))
The canonical map T ⊗[R] eq(f, g) →ₐ[S] eq (𝟙 ⊗ f, 𝟙 ⊗ g).
Equations
- AlgHom.tensorEqualizer S T f g = AlgHom.ofLinearMap (AlgHom.tensorEqualizerAux✝ S T f g) ⋯ ⋯
Instances For
@[simp]
theorem
AlgHom.coe_tensorEqualizer
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(T : Type u_3)
[CommRing T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
{A : Type u_4}
{B : Type u_5}
[CommRing A]
[CommRing B]
[Algebra R A]
[Algebra R B]
(f g : A →ₐ[R] B)
(x : TensorProduct R T ↥(equalizer f g))
:
↑((tensorEqualizer S T f g) x) = (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) x
def
AlgHom.tensorEqualizerEquiv
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(T : Type u_3)
[CommRing T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
{A : Type u_4}
{B : Type u_5}
[CommRing A]
[CommRing B]
[Algebra R A]
[Algebra R B]
(f g : A →ₐ[R] B)
[Module.Flat R T]
:
TensorProduct R T ↥(equalizer f g) ≃ₐ[S] ↥(equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f) (Algebra.TensorProduct.map (AlgHom.id S T) g))
If T is R-flat, the canonical map
T ⊗[R] eq(f, g) →ₐ[S] eq (𝟙 ⊗ f, 𝟙 ⊗ g) is an isomorphism.
Equations
- AlgHom.tensorEqualizerEquiv S T f g = AlgEquiv.ofLinearEquiv (LinearMap.tensorEqLocusEquiv S T f.toLinearMap g.toLinearMap) ⋯ ⋯
Instances For
@[simp]
theorem
AlgHom.tensorEqualizerEquiv_apply
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(T : Type u_3)
[CommRing T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
{A : Type u_4}
{B : Type u_5}
[CommRing A]
[CommRing B]
[Algebra R A]
[Algebra R B]
(f g : A →ₐ[R] B)
[Module.Flat R T]
(x : TensorProduct R T ↥(equalizer f g))
:
(tensorEqualizerEquiv S T f g) x = (tensorEqualizer S T f g) x