OAI/AlgebraicGeometry/StableCoordinate/DeterminantUFD.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Unique factorization in the determinant ring

The prime element a has a localization which is a polynomial algebra over a localization of a polynomial algebra. Nagata's prime-element criterion then proves unique factorization in the actual determinant quotient.

  1. instance OAI.StableCoordinate.DeterminantRing.C_isNoetherianRing line 21
  2. instance OAI.StableCoordinate.DeterminantRing.C_uniqueFactorizationMonoid line 23
  3. instance OAI.StableCoordinate.Obstruction.C_isNoetherianRing line 33
  4. instance OAI.StableCoordinate.Obstruction.C_uniqueFactorizationMonoid line 38

    Source documentation

    The canonical obstruction presentation is definitionally the determinant ring.

    noncomputable instance C_uniqueFactorizationMonoid : UniqueFactorizationMonoid (C k) :=
…

    Mentions: OAI.StableCoordinate.Obstruction.C