Gorenstein Local Ring

Stream: mathlib4

[Nailin Guan]

I am here to anounce that we formalized the definition of Gorenstein local ring and proved it is Cohen Macaulay in PR #30931. Our formalization follows the book "Cohen-Macaulay rings" proving dim(M) <= injdim(M) = depth(R) for finitely generated module with finite injective dimension.
We there are only few sorries left about map between Ext induced by an exact functor. (Commute with mk_0, comp and extClass)

[Nailin Guan]

Sorry, one more "sorry" : flat base change commute with Hom when finitely presented, do any one have good idea about how to implement?

[Andrew Yang]

I thought we had that? Or maybe I cheated and I only did localization. But you can probably still mimic the strategy.

[Nailin Guan]

Andrew Yang 說：

I thought we had that? Or maybe I cheated and I only did localization. But you can probably still mimic the strategy.

I think we only have localization version, I'll try study it.

[Nailin Guan]

We currently finished filling commute with mk_0 and comp, the other two sorries may need some more time.

[Nailin Guan]

We just finished proving the commute with extClass.
Now we are only left to prove flat base change commute with Hom when finitely presented and F is exact implies F.mapHomologicalComplex is exact.

[Nailin Guan]

We filled in almost all the sorries, we are only left to show the left exactness of Hom, we searched using loogle but found nothing. Do anyone know whether it exists? If not we will start a separate PR to add it then.

[Kenny Lau]

#Is there code for X? > left exactness of hom

[Kenny Lau]

do you have #mwe?

[Nailin Guan]

some thing like this:

universe u

variable (R : Type u) [CommRing R]

section

variable {R} {M1 M2 M3 : Type*} (N : Type*) [AddCommGroup M1] [AddCommGroup M2] [AddCommGroup M3]
  [AddCommGroup N] [Module R M1] [Module R M2] [Module R M3] [Module R N]

lemma lcomp_exact_of_exact_of_surjective (f : M1 →ₗ[R] M2) (g : M2 →ₗ[R] M3)
    (exac : Function.Exact f g) (surj : Function.Surjective g) :
    Function.Exact (LinearMap.lcomp R N g) (LinearMap.lcomp R N f) := by
  sorry

lemma lcomp_injective_of_surjective (g : M2 →ₗ[R] M3) (surj : Function.Surjective g) :
    Function.Injective (LinearMap.lcomp R N g) := by
  rw [← LinearMap.ker_eq_bot, eq_bot_iff]
  intro h hh
  simp only [LinearMap.mem_ker, LinearMap.lcomp_apply'] at hh
  simp only [Submodule.mem_bot]
  ext x
  rcases surj x with ⟨y, hy⟩
  rw [← hy, LinearMap.zero_apply, ← LinearMap.comp_apply, hh, LinearMap.zero_apply]

end

It is not hard though.
(We need the non-category version for this lemma
Nailin Guan 說：

Sorry, one more "sorry" : flat base change commute with Hom when finitely presented, do any one have good idea about how to implement?

[Kenny Lau]

yeah if you don't post #mwe there's no way to know if you want the category version or not

[Nailin Guan]

We have the proof now, but we want to know whether we are duplicating something.

[Kenny Lau]

@Nailin Guan Ext exists so left exactness must be somewhere

[Nailin Guan]

Ext is defined by ShiftedHom instead of plain right derived functor, there isn't clear relation to this.

[Christian Merten]

The Ext Kenny is linking to is the old (deprecated) implementation of Ext, which is a plain derived functor of docs#CategoryTheory.linearYoneda. But docs#CategoryTheory.Functor.leftDerived does not require any exactness.

[Nailin Guan]

We opened PR #31218 for left exactness of Hom.

[Kenny Lau]

@Nailin Guan I haven't thought about it, but would it be easier to use the theorem I cited in the other thread?

[Christian Merten]

By which you mean docs#LinearMap.cancel_right, I guess.

[Kenny Lau]

sorry, I meant the theorem that you only need to check it for a (standard) short exact sequence

[Kenny Lau]

do we have a "standard short exact sequence"? (i.e. where A is a submodule of B, and C is the quotient) do we know that every SES is isomorphic to a standard SES?

[Kenny Lau]

ah but there would be universe issues...

[Aaron Liu]

Kenny Lau said:

do we have a "standard short exact sequence"? (i.e. where A is a submodule of B, and C is the quotient) do we know that every SES is isomorphic to a standard SES?

Is this in specifically the context of R-Mod or is it in any abelian category?

[Kenny Lau]

R-Mod

[Nailin Guan]

We just finished all the separating, now the series consist of
#30532, #30931, #31046, #31218, #31219, #31222

[Nailin Guan]

Maybe not a very appropriate place, but some overview of all the related stuffs
6a1c4ef01997ee0290a64602270d78d6.jpg

[Nailin Guan]

Some updates.
edc201e6ab6b7cec860523a467e16c24.jpg
The next step would be proving Gorenstein local ring is stable under ring isomorphism. It turns out being a bit hard, as it involve relation of Ext over different rings.
Further goal would be proving Gorenstein local ring is atable under localization.

[Nailin Guan]

We finished proving localization of Gorenstein local ring at prime is again Gorenstein.
There are some refactor to the dependencies.
5c95d16afaa1e66b508d1761657df73e.jpg
Next step would be proving Gorenstein is stable under quotient by regular element and taking polynomial.

[Kevin Buzzard]

Let me again say that it's absolutely brilliant that you're developing all this advanced commutative algebra. Thank you! This stuff forms the basis of modern algebraic geometry, and I will also need things like Auslander--Buchsbaum for FLT.

[Nailin Guan]

The remaining problem here is that I am a bit hard to push forward constructions, update version, address review at the same time.
Currently I am trying to split things out more. I think we should get started in merging the Cohen--Macaulay part into Mathlib.

[Nailin Guan]

May I ask for a quick review for #32101? It is a stupid lemma that causing many of my branches diverging from master, wasting a lot of time to build.

[Nailin Guan]

We proved Gorenstein is stable under quotient by regular element in the PR proving it is CM, as a portion of the proof overlaps. Dependency is updated to the following.
357721d493880aa0bd14eb10685aaa3e.jpg

[Nailin Guan]

We proved that polynomial over Gorenstein ring is Gorenstein.
9d4b89eca702739422eb640fd7834091.jpg

[Nailin Guan]

As we currently not planning to move forward to dualizing complex, our reference almost ran out here, except the full version of the following (we currently have equivalece of 1, 1', 3).
If anybody found other useful results about Gorenstein ring, feel free to pin me in this thread.
图片.png

[Nailin Guan]

One more technical problem: what is the ideal way of decribing the k rank of Ext(k,M) (since it is annihilate by m)?
We currently state it as (⊤ : Submodule R ...).IsPrincipal (we know it is nontrivial, so it is equivalent in this case)

[Nailin Guan]

Can anybody help review #28582 again? This is also a deep diverging seperated out.

[Nailin Guan]

We finished the proof of above big TFAE in #32418.
For the coming days I would focus more on maintaining the PRs to get them into Mathlib.

[Nailin Guan]

After a full update, the dependencies are as the following:
b444adbed6915f0d9aaf21c8f94bcc58.jpg