Documentation

Mathlib.RingTheory.Flat.Equalizer

Base change along flat modules preserves equalizers #

We show that base change along flat modules (resp. algebras) preserves kernels and equalizers.

source
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)
source
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)
source
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
    Instances For
      source
      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
        Instances For
          source
          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
              source
              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
                  source
                  @[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
                  source
                  @[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
                  source
                  @[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
                  source
                  @[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
                  source
                  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
                    Instances For
                      source
                      @[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
                      source
                      @[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
                      source
                      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
                        Instances For
                          source
                          @[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
                          source
                          @[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
                          source
                          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
                            Instances For
                              source
                              @[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
                              source
                              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
                                Instances For
                                  source
                                  @[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