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.

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) : M →ₗ[S] ↥(ker f) →ₗ[R] ↥(ker ((TensorProduct.AlgebraTensorModule.lTensor S M) f))

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' := ⋯ }

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

• LinearMap.tensorEqLocus S M f g = TensorProduct.AlgebraTensorModule.lift (LinearMap.tensorEqLocusBil S M f g)

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

• LinearMap.tensorKer S M f = TensorProduct.AlgebraTensorModule.lift (LinearMap.tensorKerBil S M f)

@[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)) : ↑((tensorKer S M f) (m ⊗ₜ[R] x)) = m ⊗ₜ[R] ↑x

@[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)) : ↑((tensorKer S M f) x) = (lTensor M (ker f).subtype) x

@[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)) : ↑((tensorEqLocus S M f g) (m ⊗ₜ[R] x)) = m ⊗ₜ[R] ↑x

@[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) ⋯ ⋯

@[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) ⋯ ⋯

@[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) ⋯ ⋯

@[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) ⋯ ⋯

@[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