Localization commutes with tensor products

Stream: Is there code for X?

[Dion Leijnse]

I am trying to prove that the localization of a geometrically reduced algebra is again geometrically reduced. Being geometrically reduced is defined in the following way:

class IsGeometricallyReduced (k A : Type*) [Field k] [Ring A] [Algebra k A] : Prop where
  isReduced_algebraicClosure_tensorProduct : IsReduced (AlgebraicClosure k ⊗[k] A)

The proof of the result boils down to the fact that localization commutes with tensor products. Here there are some choices. Suppose we have a field k, two commutative k-algebras A and B, a submonoid M : Submonoid A, and these satisfy [IsLocalization M B]. I found two ways to state that, for a commutative k- algebra R the tensor product, R ⊗[k] B is a localization of R ⊗[k] A:

1. We let M' be the image of Munder the map A → R ⊗[k] A, and then we want that R ⊗[k] B is the localization of R ⊗[k] A with respect to M'. This can be formalized as:

let M' : Submonoid (R ⊗[k] A) :=
    M.map Algebra.TensorProduct.includeRight.toRingHom.toMonoidHom
example : IsLocalization M' (R ⊗[k] B)

2. Turn R ⊗[k] A into an A- algebra, and then we can write

IsLocalization (algebraMapSubmonoid (R ⊗[k] A) M) (R ⊗[k] B)

To me the second way seems to be the better way to go given the current results in Mathlib. In particular, I can use Algebra.isLocalization_iff_isPushout to reduce to showing that something is a pushout. However, when doing this, I need to manually provide a lot of instances of Algebra and IsScalarTower. And then when I actually try to prove that the thing I want to be a pushout is actually a pushout (see code below), I need to provide even more instances manually. Is there a more efficient way to do this, or do all these manual instances really have to be provided?

Here is the full code:

import Mathlib

open TensorProduct

namespace Algebra

/-- The `k`-algebra `A` is geometrically reduced iff its base change to `AlgebraicClosure k` is
  reduced. -/
@[mk_iff]
class IsGeometricallyReduced (k A : Type*) [Field k] [Ring A] [Algebra k A] : Prop where
  isReduced_algebraicClosure_tensorProduct : IsReduced (AlgebraicClosure k ⊗[k] A)

attribute [instance] IsGeometricallyReduced.isReduced_algebraicClosure_tensorProduct

variable (k A B R : Type) [Field k] [CommRing R] [CommRing A] [CommRing B] (S : Submonoid A)
    [Algebra A B] [Algebra k A] [Algebra k B] [IsScalarTower k A B] [IsLocalization S B]
    [Algebra k R]

-- corresponds with the first way of taking localization
theorem IsGeometricallyReduced.of_localization2 {k A B : Type} [CommRing B] [CommRing A]
    [h : Algebra A B] [Field k] [Algebra k A] [Algebra k B] [IsScalarTower k A B] {M : Submonoid A}
    [Algebra.IsGeometricallyReduced k A] [IsLocalization M B] :
    Algebra.IsGeometricallyReduced k B := by
  have : Algebra (AlgebraicClosure k ⊗[k] A) (AlgebraicClosure k ⊗[k] B) :=
    RingHom.toAlgebra (Algebra.TensorProduct.map
      (AlgHom.id k (AlgebraicClosure k)) (Algebra.algHom k A B))
  let M' : Submonoid (AlgebraicClosure k ⊗[k] A) :=
    M.map Algebra.TensorProduct.includeRight.toRingHom.toMonoidHom
  have hLoc : IsLocalization M' (AlgebraicClosure k ⊗[k] B) := by
    sorry
  rw [Algebra.isGeometricallyReduced_iff]
  apply isReduced_localizationPreserves M' (AlgebraicClosure k ⊗[k] B)
  infer_instance

-- corresponds with the second way of taking the localization
theorem IsGeometricallyReduced.of_localization {k A B : Type} [CommRing B] [CommRing A]
    [h : Algebra A B] [Field k] [Algebra k A] [Algebra k B] [IsScalarTower k A B] {M : Submonoid A}
    [Algebra.IsGeometricallyReduced k A] [IsLocalization M B] :
    Algebra.IsGeometricallyReduced k B := by
  have : Algebra (AlgebraicClosure k ⊗[k] A) (AlgebraicClosure k ⊗[k] B) :=
    RingHom.toAlgebra (Algebra.TensorProduct.map
      (AlgHom.id k (AlgebraicClosure k)) (Algebra.algHom k A B))
  have : Algebra A (AlgebraicClosure k ⊗[k] A) :=
    RingHom.toAlgebra (TensorProduct.includeRight : A →ₐ[k] AlgebraicClosure k ⊗[k] A)
  have : Algebra A (AlgebraicClosure k ⊗[k] B) := RingHom.toAlgebra
    ((TensorProduct.includeRight : B →ₐ[k] AlgebraicClosure k ⊗[k] B).toRingHom.comp
    (RingHom.smulOneHom : A →+* B))
  have : Algebra B (AlgebraicClosure k ⊗[k] B) :=
    RingHom.toAlgebra (TensorProduct.includeRight : B →ₐ[k] AlgebraicClosure k ⊗[k] B)
  have : IsScalarTower A (AlgebraicClosure k ⊗[k] A) (AlgebraicClosure k ⊗[k] B) := by
    sorry
  have : IsScalarTower A B (AlgebraicClosure k ⊗[k] B) := by sorry

  have hLoc' : IsLocalization (algebraMapSubmonoid (AlgebraicClosure k ⊗[k] A) M)
      (AlgebraicClosure k ⊗[k] B) := by
    rw [isLocalization_iff_isPushout M B]
    -- Current goal:
    --   ⊢ IsPushout A (AlgebraicClosure k ⊗[k] A) B (AlgebraicClosure k ⊗[k] B)
    sorry
  rw [Algebra.isGeometricallyReduced_iff]
  apply isReduced_localizationPreserves (algebraMapSubmonoid (AlgebraicClosure k ⊗[k] A) M)
      (AlgebraicClosure k ⊗[k] B)
  infer_instance

[Junyan Xu]

A possible solution:

open Algebra.TensorProduct in
theorem IsGeometricallyReduced.of_localization {k A B : Type} [CommRing B] [CommRing A]
    [h : Algebra A B] [Field k] [Algebra k A] [Algebra k B] [IsScalarTower k A B] {M : Submonoid A}
    [Algebra.IsGeometricallyReduced k A] [IsLocalization M B] :
    Algebra.IsGeometricallyReduced k B := by
  rw [Algebra.isGeometricallyReduced_iff]
  set kbar := AlgebraicClosure k
  have : IsReduced (B ⊗[A] (A ⊗[k] kbar)) :=
    let _ := @rightAlgebra
    isReduced_localizationPreserves (algebraMapSubmonoid (A ⊗[k] kbar) M)
      (B ⊗[A] (A ⊗[k] kbar)) (isReduced_of_injective _ (TensorProduct.comm ..).injective)
  have e₁ := TensorProduct.congr (.refl (R := k) (A₁ := kbar)) ((TensorProduct.rid A A B).restrictScalars k)
  have e₂ := (TensorProduct.comm ..).trans <| (TensorProduct.assoc k A B A kbar).restrictScalars k
  exact isReduced_of_injective _ (e₁.symm.trans e₂).injective

I'd expect some of the Algebra.TensorProduct defs could be generalized to make this smoother.

[Junyan Xu]

By the way, why are you using have (not let) for data like Algebra that are later used in IsScalarTower?

[Dion Leijnse]

Thanks, that looks a lot cleaner than what I was trying! I mostly used have because I didn't know when to use let vs have.

[Kenny Lau]

@Dion Leijnse the rule of thumb is that you use let when the thing contains data, and have when it's just a theorem

[Dion Leijnse]

Thanks!

[Junyan Xu]

I'm breaking that rule, since I just want the existence of an AlgEquiv (MulEquiv would be enough actually).

[Junyan Xu]

By the way we should have a universe polymorphic version of isReduced_localizationPreserves (just like IsLocalization.noZeroDivisors etc.)

[Kenny Lau]

Sure, but before you break the rule you have to know the rule