an algebra that is module-invertible is the base ring

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

variable (R A : Type*) [CommRing R] [CommRing A] [Algebra R A] [Module.Invertible R A]

def algEquivOfInvertible : R ≃ₐ[R] A :=
  sorry

[Kenny Lau]

import Mathlib

def LinearEquiv.algEquiv {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
    (e : R ≃ₗ[R] A) : R ≃ₐ[R] A where
  __ := Algebra.ofId R A
  invFun := (e.symm : A →ₗ[R] R) ∘ₗ Algebra.lmul R A (e 1)
  left_inv x := calc
    e.symm (e 1 * (algebraMap R A) x)
      = e.symm (x • e 1) := by rw [Algebra.smul_def, mul_comm]
    _ = x := by rw [map_smul, e.symm_apply_apply, smul_eq_mul, mul_one]
  right_inv x := calc
    (algebraMap R A) (e.symm (e 1 * x))
      = (algebraMap R A) (e.symm (e 1 * x)) * e (e.symm 1 • 1) := by
          rw [smul_eq_mul, mul_one, e.apply_symm_apply, mul_one]
    _ = x := by rw [map_smul, Algebra.smul_def, mul_left_comm, ← Algebra.smul_def _ (e 1),
          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, ← mul_assoc, ← Algebra.smul_def,
          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, one_mul]

instance isLocalizedModule_ofId {R : Type*} [CommSemiring R] (S : Submonoid R) :
    IsLocalizedModule S (Algebra.linearMap R (Localization S)) := by
  refine isLocalizedModule_iff_isLocalization.mpr ?_
  convert Localization.isLocalization
  exact S.map_id

theorem Module.Invertible.of_isLocalization (R R' M M' : Type*)
    [CommRing R] (S : Submonoid R) [CommRing R'] [Algebra R R'] [IsLocalization S R']
    [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M']
    (f : M →ₗ[R] M') [IsLocalizedModule S f] [Module R' M'] [IsScalarTower R R' M']
    [Module.Invertible R M] : Module.Invertible R' M' :=
  .congr (IsBaseChange.equiv <| IsLocalizedModule.isBaseChange S R' f)

variable (R A : Type*) [CommRing R] [CommRing A] [Algebra R A] [Module.Invertible R A]

private theorem bijective_ofId_of_isLocalRing [IsLocalRing R] :
    Function.Bijective (Algebra.ofId R A) :=
  let ⟨e⟩ := (Module.Invertible.free_iff_linearEquiv (R := R) (M := A)).mp inferInstance
  e.symm.algEquiv.bijective

noncomputable def algEquivOfInvertible : R ≃ₐ[R] A :=
  .ofBijective (Algebra.ofId R A) <| by
    refine bijective_of_isLocalized_maximal
      (fun P _ ↦ Localization.AtPrime P)
      (fun P _ ↦ Algebra.linearMap R (Localization.AtPrime P))
      (fun P _ ↦ LocalizedModule P.primeCompl A)
      (fun P _ ↦ LocalizedModule.mkLinearMap _ _)
      (Algebra.linearMap R A)
      fun P _ ↦ ?_
    have : Module.Invertible (Localization.AtPrime P) (LocalizedModule P.primeCompl A) :=
      Module.Invertible.of_isLocalization _ _ _ _ P.primeCompl (LocalizedModule.mkLinearMap _ _)
    convert bijective_ofId_of_isLocalRing (Localization.AtPrime P) (LocalizedModule P.primeCompl A)
    ext x
    induction' x using Localization.induction_on with frac
    rw [Algebra.ofId_apply, Localization.mk_eq_mk', LocalizedModule.algebraMap_mk', IsLocalization.mk'_eq_mk', IsLocalizedModule.map_mk', IsLocalizedModule.mk_eq_mk']
    rfl

[Kenny Lau]

So #find_home! algEquivOfInvertible returned "Mathlib" which i take to mean that this belongs to a new file

[Kenny Lau]

@Aaron Liu would you agree?

[Aaron Liu]

Module.Invertible is defined in Mathlib.RingTheory.PicardGroup which is imported by no other files

[Aaron Liu]

if it doesn't massively increase the imports you could maybe put it there

[Kenny Lau]

i mean in general i'm in the camp of "let's split to as many files as possible to keep the imports small in each file"

[Aaron Liu]

or we move Module.Invertible somewhere else

[Kenny Lau]

Kenny Lau said:

i mean in general i'm in the camp of "let's split to as many files as possible to keep the imports small in each file"

image.png

never mind...

[Kenny Lau]

#29954

[Ruben Van de Velde]

It seems plausible that Module.Invertible could be defined in a separate, lighter file but the file isn't that big yet, so this is probably fine for now

[Kenny Lau]

so i realised that there is a more straightforward proof that should work for semirings

[Kenny Lau]

update: i realised while writing the proof on paper that I implicitly assumed for all x : A, 1 ⊗ₜ x = x ⊗ₜ 1, which is equivalent to the result (and equivalent to R -> A being an epimorphism of semirings)

[Aaron Liu]

Interesting

[Aaron Liu]

Can you fix it

[Kenny Lau]

so I'm able to make an R-linear map r : A -> R with r(1) = 1, so R -> A -> R is identity, but I can't prove that A -> R -> A is identity

[Kenny Lau]

fun fact, Nat is a local ring?!?!

[Kenny Lau]

and if you make 2 invertible, then 3/8 + 5/8 = 1, so the localization of a local ring is not a local ring?!?!

[Aaron Liu]

What's the definition of local ring again I think they might not be equivalent for semirings

[Kenny Lau]

/-- A semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.
Note that `IsLocalRing` is a predicate. -/
class IsLocalRing (R : Type*) [Semiring R] : Prop extends Nontrivial R where
  of_is_unit_or_is_unit_of_add_one ::
  /-- in a local ring `R`, if `a + b = 1`, then either `a` is a unit or `b` is a unit. In another
  word, for every `a : R`, either `a` is a unit or `1 - a` is a unit. -/
  isUnit_or_isUnit_of_add_one {a b : R} (h : a + b = 1) : IsUnit a ∨ IsUnit b

[Kenny Lau]

so 2N is not a maximal ideal of N...

[Aaron Liu]

The maximal ideal is the nonzero nonone numbers

[Kenny Lau]

include 0

[Aaron Liu]

the nonone numbers

[Aaron Liu]

you need zero to be an ideal

[Kenny Lau]

so in fact there is exactly one maximal ideal of Nat :D

[Kenny Lau]

image.png

[Kenny Lau]

yeah, what on earth, this equivalence holds for comm semirings

[Aaron Liu]

Oh that's just great

[Aaron Liu]

I've realized I didn't actually have any nontrivial examples of invertible modules

[Kenny Lau]

and I have never thought about invertible modules over commutative semirings

[Kenny Lau]

Aaron Liu said:

I've realized I didn't actually have any nontrivial examples of invertible modules

it's related to class groups which is related to quadratic forms

[Johan Commelin]

Yeah, class group is the key concept here.

[Kenny Lau]

or you can use dedekind rings, from number fields

[Aaron Liu]

Sure but I don't know very much about those either

[Kenny Lau]

so you can use 2*3 = (1+r(-5))(1-r(-5)) (r = sqrt)

[Aaron Liu]

What does that do for me

[Kenny Lau]

and then the ideal (2, 1+sqrt(-5)) in Z[sqrt(-5)] is not principal

[Aaron Liu]

oh yes

[Kenny Lau]

@Aaron Liu you can search by class group on LMFDB

[Kenny Lau]

I think I have a proof now

[Aaron Liu]

Oh I think I figured out how to go from nonprincipal ideal to invertible module

[Kenny Lau]

import Mathlib

namespace Module.Invertible

variable {R M N : Type*} [CommSemiring R]
  [AddCommMonoid M] [Module R M] [Module.Invertible R M]
  [AddCommMonoid N] [Module R N] [Module.Invertible R N]

variable {f : M →ₗ[R] N} {g : N →ₗ[R] M}

theorem rightInverse_of_leftInverse (hfg : Function.LeftInverse f g) :
    Function.RightInverse f g :=
  Function.rightInverse_of_injective_of_leftInverse
    (bijective_of_surjective hfg.surjective).injective hfg

theorem leftInverse_of_rightInverse (hfg : Function.RightInverse f g) :
    Function.LeftInverse f g :=
  rightInverse_of_leftInverse hfg

variable (f g) in
theorem leftInverse_iff_rightInverse :
    Function.LeftInverse f g ↔ Function.RightInverse f g :=
  ⟨rightInverse_of_leftInverse, leftInverse_of_rightInverse⟩

def linearEquivOfLeftInverse (hfg : Function.LeftInverse f g) : M ≃ₗ[R] N :=
  .ofLinear f g (LinearMap.ext hfg) (LinearMap.ext <| rightInverse_of_leftInverse hfg)

def linearEquivOfRightInverse (hfg : Function.RightInverse f g) : M ≃ₗ[R] N :=
  .ofLinear f g (LinearMap.ext <| leftInverse_of_rightInverse hfg) (LinearMap.ext hfg)

variable (R) (A : Type*) [Semiring A] [Algebra R A] [Module.Invertible R A]

open TensorProduct

set_option synthInstance.maxHeartbeats 99999 in
/-- The algebra structure gives us a map `A ⊗ A → A`, which after tensoring by `Aᵛ` becomes a map
`A → R`, which is the inverse map we seek. -/
noncomputable def algEquivOfRing : R ≃ₐ[R] A :=
  let inv : A →ₗ[R] R :=
    linearEquiv R A ∘ₗ
      (LinearMap.mul' R A).lTensor (Dual R A) ∘ₗ
      (leftCancelEquiv A (linearEquiv R A)).symm
  have right : inv ∘ₗ Algebra.linearMap R A = LinearMap.id :=
    let ⟨s, hs⟩ := exists_finset ((linearEquiv R A).symm 1)
    LinearMap.ext_ring <| by simp [inv, hs, sum_tmul, map_sum, ← (LinearEquiv.symm_apply_eq _).1 hs]
  { linearEquivOfRightInverse (f := Algebra.linearMap R A) (g := inv) (LinearMap.ext_iff.1 right),
    Algebra.ofId R A with }

end Module.Invertible

[Kenny Lau]

updated #29954

[Aaron Liu]

99999 is a bit as scary what's the usual number

[Kenny Lau]

20000

[Kenny Lau]

it's in the same order of magnitude

[Aaron Liu]

oh that's good

[Kenny Lau]

apparently it's only needed if i import Mathlib; in the PR where i work locally in the file, i don't need to set the max heartbeats