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

The bilinear map corresponding to LinearMap.tensorEqLocus.

Equations

• LinearMap.tensorEqLocusBil S M f g = { toFun := fun (m : M) => { toFun := fun (a : ↥(f.eqLocus g)) => ⟨m ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

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.

Equations

• LinearMap.tensorKerBil S M f = { toFun := fun (m : M) => { toFun := fun (a : ↥f.ker) => ⟨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 ↥(f.eqLocus g) →ₗ[S] ↥(((TensorProduct.AlgebraTensorModule.lTensor S M) f).eqLocus ((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 ↥f.ker →ₗ[S] ↥((TensorProduct.AlgebraTensorModule.lTensor S M) f).ker

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 : ↥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 : ↥(f.eqLocus 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 ↥(f.eqLocus g)) : ↑((tensorEqLocus S M f g) x) = (lTensor M (f.eqLocus g).subtype) x

noncomputable def LinearMap.tensorKerInv {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.AlgebraTensorModule.lTensor S M) f).ker →ₗ[S] TensorProduct R M ↥f.ker

(Implementation): Inverse for LinearMap.tensorKerEquiv.

Equations

• LinearMap.tensorKerInv S M f = ((TensorProduct.AlgebraTensorModule.lTensor S M) f).ker.subtype.codRestrictOfInjective ((TensorProduct.AlgebraTensorModule.lTensor S M) f.ker.subtype) ⋯ ⋯

noncomputable def LinearMap.tensorEqLocusInv {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.AlgebraTensorModule.lTensor S M) f).eqLocus ((TensorProduct.AlgebraTensorModule.lTensor S M) g)) →ₗ[S] TensorProduct R M ↥(f.eqLocus g)

(Implementation): Inverse for LinearMap.tensorEqLocusEquiv.

Equations

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

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

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 ↥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

noncomputable 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 ↥(f.eqLocus g) ≃ₗ[S] ↥(((TensorProduct.AlgebraTensorModule.lTensor S M) f).eqLocus ((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 ↥(f.eqLocus 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 : ↥(((TensorProduct.AlgebraTensorModule.lTensor S M) f).eqLocus ((TensorProduct.AlgebraTensorModule.lTensor S M) g))) : (lTensor M (f.eqLocus 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.

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

Equations

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

@[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.tensorEqualizerAux {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 ↥(f.equalizer g) →ₗ[S] ↥((Algebra.TensorProduct.map (AlgHom.id S T) f).equalizer (Algebra.TensorProduct.map (AlgHom.id S T) g))

(Implementation): Use AlgHom.tensorEqualizer instead.

Equations

• AlgHom.tensorEqualizerAux S T f g = LinearMap.tensorEqLocus S T ↑f ↑g

theorem AlgHom.tensorEqualizerAux_mul {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 y : TensorProduct R T ↥(f.equalizer g)) : (tensorEqualizerAux S T f g) (x * y) = (tensorEqualizerAux S T f g) x * (tensorEqualizerAux S T f g) 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 ↥(f.equalizer g) →ₐ[S] ↥((Algebra.TensorProduct.map (AlgHom.id S T) f).equalizer (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 ↥(f.equalizer g)) : ↑((tensorEqualizer S T f g) x) = (Algebra.TensorProduct.map (AlgHom.id S T) (f.equalizer g).val) x

noncomputable 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 ↥(f.equalizer g) ≃ₐ[S] ↥((Algebra.TensorProduct.map (AlgHom.id S T) f).equalizer (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 ↥(f.equalizer g)) : (tensorEqualizerEquiv S T f g) x = (tensorEqualizer S T f g) x

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

Equations

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

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

def RingHom.HasStableEqualizers (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : Prop

A property P of ring homomorphisms is said to have stable equalizers, if the equalizer of algebra maps between algebras with structure morphisms satisfying P, is preserved by arbitrary base change.

Equations

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