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] : ((TensorProduct.AlgebraTensorModule.lTensor S M) f).ker = ((TensorProduct.AlgebraTensorModule.lTensor S M) f.ker.subtype).range

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) = ((TensorProduct.AlgebraTensorModule.lTensor S M) (LinearMap.eqLocus f g).subtype).range

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.

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

The bilinear map corresponding to LinearMap.tensorKer.

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).

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

The canonical map M ⊗[R] ker f →ₗ[R] ker (𝟙 ⊗ 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 : ↥f.ker) : ↑((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 ↥f.ker) : ↑((tensorKer S M f) x) = (lTensor M f.ker.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 ↥f.ker ≃ₗ[S] ↥((TensorProduct.AlgebraTensorModule.lTensor S M) f).ker

If M is R-flat, the canonical map M ⊗[R] ker f →ₗ[R] ker (𝟙 ⊗ f) is an isomorphism.

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

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

theorem LinearMap.lTensor_injective_of_exact_of_flat {R : Type u_1} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {N : Type u_4} {P : Type u_5} [AddCommGroup N] [AddCommGroup P] [Module R N] [Module R P] [Module.Flat R P] (f : N →ₗ[R] P) (hf : Function.Surjective ⇑f) (g : M →ₗ[R] N) (hg : Function.Injective ⇑g) (H : Function.Exact ⇑g ⇑f) (A : Type u_6) [AddCommGroup A] [Module R A] : Function.Injective ⇑(lTensor A g)

Given a short exact sequence 0 → M → N → P → 0 with P flat, then any A ⊗ M → A ⊗ N is injective.

def LinearMap.kerLTensorEquivOfSurjective {R : Type u_1} [CommRing R] {N : Type u_4} {P : Type u_5} [AddCommGroup N] [AddCommGroup P] [Module R N] [Module R P] [Module.Flat R P] (f : N →ₗ[R] P) (hf : Function.Surjective ⇑f) (A : Type u_6) [AddCommGroup A] [Module R A] : ↥(lTensor A f).ker ≃ₗ[R] TensorProduct R A ↥f.ker

Given surjection f : N → P with P flat, then A ⊗ ker f ≃ ker (A ⊗ f). Also see LinearMap.tensorKerEquiv for the version with A flat instead.

@[simp]

theorem LinearMap.tensorKerEquivOfSurjective_symm_tmul {R : Type u_1} [CommRing R] {N : Type u_4} {P : Type u_5} [AddCommGroup N] [AddCommGroup P] [Module R N] [Module R P] [Module.Flat R P] (f : N →ₗ[R] P) (hf : Function.Surjective ⇑f) (A : Type u_6) [AddCommGroup A] [Module R A] (a : A) (y : ↥f.ker) : ↑((f.kerLTensorEquivOfSurjective hf A).symm (a ⊗ₜ[R] y)) = a ⊗ₜ[R] ↑y

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).

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

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

def Algebra.kerTensorProductMapIdToAlgHomEquiv (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) [CommRing A] [Algebra R A] [Module.Flat R T] (h₁ : Function.Surjective ⇑(algebraMap S T)) : ↥(RingHom.ker (TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T))) ≃ₗ[TensorProduct R A S] TensorProduct S (TensorProduct R A S) ↥(RingHom.ker (algebraMap S T))

Given a surjection of R-algebras S → T with kernel I, such that T is flat, the kernel of the map A ⊗ S → A ⊗ T is the base change of I along S → A ⊗ S.

@[simp]

theorem Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_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} [CommRing A] [Algebra R A] [Module.Flat R T] (h₁ : Function.Surjective ⇑(algebraMap S T)) (x : A) (y : S) (z : ↥(RingHom.ker (algebraMap S T))) : ↑((kerTensorProductMapIdToAlgHomEquiv R S T A h₁).symm (x ⊗ₜ[R] y ⊗ₜ[S] z)) = x ⊗ₜ[R] (y * ↑z)