construct a bilinear map of A algebras

Stream: new members

[Xipan Xiao]

I was trying to prove that S⁻¹A ⊗ₐ M and S⁻¹Mare isomorphic as an S⁻¹A module, first I wrote the goal and sketched the proof, like:

import Mathlib

open TensorProduct

variable {A : Type*} [CommRing A] (S : Submonoid A)
variable (M : Type*) [AddCommGroup M] [Module A M]

noncomputable def localizationTensorEquivLocalizationModule :
  Localization S ⊗[A] M ≃ₗ[Localization S] LocalizedModule S M := by
  have hom : Localization S ⊗[A] M →ₗ[Localization S] LocalizedModule S M := sorry
  have inv : LocalizedModule S M →ₗ[Localization S] Localization S ⊗[A] M := by sorry
  have left_inv : Function.LeftInverse inv hom := by sorry
  have right_inv : Function.RightInverse inv hom := by sorry
  exact {
    toFun := hom,
    invFun := inv,
    left_inv := left_inv,
    right_inv := right_inv,
    map_add' := by simp,
    map_smul' := by simp
  }

Then I tried to construct the homomorphism Localization S ⊗[A] M →ₗ[Localization S] LocalizedModule S M but I didn't make it. Mathematically I know this is the ring map induced from the bilinear map (x, m)\mapsto xm from S⁻¹A × M to S⁻¹M, but I don't know how to express in lean. I tried something like TensorProduct.lift bilinearMap but I don't know how to construct the bilinear map. I tried

  let bilinearMap : Localization S × M → LocalizedModule S M :=
    LinearMap.mk₂ A (fun x m => x * m)
    (by intros x₁ x₂ m; sorry)
    (by intros a x m; sorry)
    (by intros x m₁ m₂; sorry)
    (by intros a x m; sorry)

but kept struggling with type errors with some weird characters or failed to synthesize. Any hints are appreciated. Thanks.

[Junyan Xu]

I was trying to prove that S⁻¹A ⊗ₐ M and S⁻¹Mare isomorphic as an S⁻¹A algebra, ...

I think you mean they are isomorphic as S⁻¹A-modules, because S⁻¹M isn't a ring.

bilinearMap : Localization S × M → LocalizedModule S M doesn't match the type of LinearMap.mk₂, so you'll certainly get errors. You probably want bilinearMap : Localization S →ₗ[Localization S] M →ₗ[Localization S] LocalizedModule S M.

[Junyan Xu]

What you want is already available in mathlib as LocalizedModule.equivTensorProduct, by the way.