NYLL
Module

IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
31 declarations indexed from sourceView source ↗

Module documentation

Is Regular Ring unique Factorization Monoid of is Local Ring

Imports15
Imported by2

Declarations

lemma

length_le_depth

L48 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.DepthLemma.length_le_depth
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace DepthLemma
variable {R : Type*} [CommRing R] [IsLocalRing R]
Lean source · statement
lemma length_le_depth {M : Type*} [AddCommGroup M] [Module R M] {rs : List R}
    (h1 : IsWeaklyRegular M rs) (h2 : ∀ r ∈ rs, r ∈ maximalIdeal R) :
    (rs.length : ℕ∞) ≤ Module.depth R M
lemma

exists_isSMulRegular_of_one_le_depth

L53 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.DepthLemma.exists_isSMulRegular_of_one_le_depth
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace DepthLemma
variable {R : Type*} [CommRing R] [IsLocalRing R]
Lean source · statement
lemma exists_isSMulRegular_of_one_le_depth {M : Type*} [AddCommGroup M] [Module R M]
    (h : 1 ≤ Module.depth R M) : ∃ x ∈ maximalIdeal R, IsSMulRegular M x
lemma

not_isAssociatedPrime_of_isSMulRegular

L66 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.DepthLemma.not_isAssociatedPrime_of_isSMulRegular
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace DepthLemma
variable {R : Type*} [CommRing R] [IsLocalRing R]
Lean source · statement
lemma not_isAssociatedPrime_of_isSMulRegular [IsNoetherianRing R]
    {M : Type*} [AddCommGroup M] [Module R M]
    {x : R} (hx : x ∈ maximalIdeal R) (hreg : IsSMulRegular M x) :
    ¬ IsAssociatedPrime (maximalIdeal R) M
theorem

core

L81 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.DepthLemma.core
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace DepthLemma
variable {R : Type*} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem core [IsNoetherianRing R] (n : ℕ) :
    ∀ {K F M : Type*} [AddCommGroup K] [Module R K] [AddCommGroup F] [Module R F]
      [Module.Finite R F] [AddCommGroup M] [Module R M]
      (f : K →ₗ[R] F) (g : F →ₗ[R] M), Function.Injective f → Function.Exact f g →
      Function.Surjective g →
      (n : ℕ∞) ≤ Module.depth R F → (n : ℕ∞) ≤ Module.depth R M + 1 →
      (n : ℕ∞) ≤ Module.depth R K
theorem

min_depth_depth_add_one_le_depth_of_exact

L144 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.DepthLemma.min_depth_depth_add_one_le_depth_of_exact
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace DepthLemma
variable {R : Type*} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem min_depth_depth_add_one_le_depth_of_exact
    {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {K F M : Type*} [AddCommGroup K] [Module R K] [AddCommGroup F] [Module R F]
    [Module.Finite R F] [AddCommGroup M] [Module R M]
    (f : K →ₗ[R] F) (g : F →ₗ[R] M) (hf : Function.Injective f) (hfg : Function.Exact f g)
    (hg : Function.Surjective g) :
    min (Module.depth R F) (Module.depth R M + 1) ≤ Module.depth R K
def

HasFFR

L173 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.HasFFR
Documentation

Existence of a finite free resolution of the specified length, defined recursively through kernels.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
Lean source · full declaration
def HasFFR (R : Type u) [CommRing R] : ℕ → (K : Type u) → [AddCommGroup K] → [Module R K] → Prop
  | 0, K, _, _ => Module.Finite R K ∧ Module.Free R K
  | n + 1, K, _, _ => ∃ (k : ℕ) (f : (Fin k → R) →ₗ[R] K),
      Function.Surjective f ∧ HasFFR R n (LinearMap.ker f)
lemma

hasFFR_zero_iff

L180 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.hasFFR_zero_iff
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
Lean source · statement
lemma hasFFR_zero_iff (K : Type u) [AddCommGroup K] [Module R K] :
    HasFFR R 0 K ↔ Module.Finite R K ∧ Module.Free R K
lemma

hasFFR_succ_iff

L183 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.hasFFR_succ_iff
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
Lean source · statement
lemma hasFFR_succ_iff (n : ℕ) (K : Type u) [AddCommGroup K] [Module R K] :
    HasFFR R (n + 1) K ↔ ∃ (k : ℕ) (f : (Fin k → R) →ₗ[R] K),
      Function.Surjective f ∧ HasFFR R n (LinearMap.ker f)
lemma

congr

L187 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.HasFFR.congr
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
Lean source · full declaration
lemma HasFFR.congr : ∀ (n : ℕ) {K K' : Type u} [AddCommGroup K] [Module R K]
    [AddCommGroup K'] [Module R K'] (_e : K ≃ₗ[R] K'), HasFFR R n K → HasFFR R n K'
  | 0, K, K', _, _, _, _, e, h => by
    rw [hasFFR_zero_iff] at h ⊢
    obtain ⟨h1, h2⟩ := h
    exact ⟨Module.Finite.equiv e, Module.Free.of_equiv e⟩
  | n + 1, K, K', _, _, _, _, e, h => by
    rw [hasFFR_succ_iff] at h ⊢
    obtain ⟨k, f, hf, hK⟩ := h
    refine ⟨k, e.toLinearMap ∘ₗ f, e.surjective.comp hf, ?_⟩
    have hker : LinearMap.ker (e.toLinearMap ∘ₗ f) = LinearMap.ker f := LinearEquiv.ker_comp e f
    exact HasFFR.congr n (LinearEquiv.ofEq _ _ hker.symm) hK
lemma

length_le_depth

L204 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.length_le_depth
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
section depth
variable [IsLocalRing R]
Lean source · statement
lemma length_le_depth {M : Type*} [AddCommGroup M] [Module R M] {rs : List R}
    (h1 : IsWeaklyRegular M rs) (h2 : ∀ r ∈ rs, r ∈ maximalIdeal R) :
    (rs.length : ℕ∞) ≤ Module.depth R M
lemma

exists_isWeaklyRegular_of_le_depth

L209 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.exists_isWeaklyRegular_of_le_depth
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
section depth
variable [IsLocalRing R]
Lean source · statement
lemma exists_isWeaklyRegular_of_le_depth {M : Type*} [AddCommGroup M] [Module R M] (n : ℕ)
    (h : (n : ℕ∞) ≤ Module.depth R M) :
    ∃ rs : List R, IsWeaklyRegular M rs ∧ (∀ r ∈ rs, r ∈ maximalIdeal R) ∧ n ≤ rs.length
lemma

depth_eq_top_of_subsingleton

L225 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.depth_eq_top_of_subsingleton
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
section depth
variable [IsLocalRing R]
Lean source · statement
lemma depth_eq_top_of_subsingleton (M : Type*) [AddCommGroup M] [Module R M] [Subsingleton M] :
    Module.depth R M = ⊤
lemma

le_depth_pi

L240 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.le_depth_pi
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
Lean source · statement
lemma le_depth_pi [IsRegularLocalRing R] (d : ℕ) (hd : ringKrullDim R = d) (k : ℕ) :
    (d : ℕ∞) ≤ Module.depth R (Fin k → R)
theorem

hasFFR_of_le_depth

L258 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.hasFFR_of_le_depth
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
section syzygy
variable [IsRegularLocalRing R]
Lean source · statement
theorem hasFFR_of_le_depth (d : ℕ) (hd : ringKrullDim R = d) :
    ∀ n : ℕ, n ≤ d → ∀ (K : Type u) [AddCommGroup K] [Module R K] [Module.Finite R K],
      ((d - n : ℕ) : ℕ∞) ≤ Module.depth R K → HasFFR R n K
theorem

hasFFR

L293 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.hasFFR
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
section syzygy
variable [IsRegularLocalRing R]
Lean source · statement
theorem hasFFR (d : ℕ) (hd : ringKrullDim R = d) (K : Type u) [AddCommGroup K] [Module R K]
    [Module.Finite R K] : HasFFR R d K
def

kerBaseChangeEquiv

L305 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.kerBaseChangeEquiv
Documentation

The equivalence between a kernel after flat base change and the base change of the original kernel.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
section stablyFree
variable (S : Type v) [CommRing S] [Algebra R S]
Lean source · statement
def kerBaseChangeEquiv [Module.Flat R S] {K : Type w} [AddCommGroup K] [Module R K]
    {k : ℕ} (f : (Fin k → R) →ₗ[R] K) :
    S ⊗[R] (LinearMap.ker f) ≃ₗ[S] LinearMap.ker (f.baseChange S)
lemma

step

L333 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.step
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
section stablyFree
variable (S : Type v) [CommRing S] [Algebra R S]
variable {S} in
Lean source · statement
lemma step [Module.Flat R S] {K : Type w} [AddCommGroup K] [Module R K] {k : ℕ}
    (f : (Fin k → R) →ₗ[R] K) (hf : Function.Surjective f)
    [Module.Projective S (S ⊗[R] K)] :
    Module.Projective S (S ⊗[R] (LinearMap.ker f)) ∧
      (Module.IsStablyFree S (S ⊗[R] (LinearMap.ker f)) → Module.IsStablyFree S (S ⊗[R] K))
theorem

isStablyFree_of_hasFFR

L379 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.isStablyFree_of_hasFFR
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
section stablyFree
variable (S : Type v) [CommRing S] [Algebra R S]
variable {S} in
Lean source · statement
theorem isStablyFree_of_hasFFR [Module.Flat R S] :
    ∀ (n : ℕ) (K : Type u) [AddCommGroup K] [Module R K] [Module.Projective S (S ⊗[R] K)],
      HasFFR R n K → Module.IsStablyFree S (S ⊗[R] K)
theorem

isStablyFree_baseChange

L398 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.StablyFree.isStablyFree_baseChange
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
Lean source · statement
theorem isStablyFree_baseChange (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (S : Type v) [CommRing S] [Algebra R S] [Module.Flat R S]
    (M : Type w) [AddCommGroup M] [Module R M] [Module.Finite R M]
    [Module.Projective S (S ⊗[R] M)] :
    Module.IsStablyFree S (S ⊗[R] M)
def

tensorIdealEquivMap

L421 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.tensorIdealEquivMap
Documentation

The equivalence between tensoring an ideal to a localization and extending the ideal there.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
section idealLoc
variable {A : Type*} [CommRing A] (M : Submonoid A) (B : Type*) [CommRing B] [Algebra A B]
  [IsLocalization M B]
Lean source · statement
def tensorIdealEquivMap (I : Ideal A) :
    B ⊗[A] I ≃ₗ[B] (I.map (algebraMap A B) : Ideal B)
def

linearEquivOfSpanSingleton

L434 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.linearEquivOfSpanSingleton
Documentation

The linear equivalence from a nonzero principal ideal in a domain to the coefficient ring.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
section principal
variable {S : Type*} [CommRing S]
Lean source · statement
def linearEquivOfSpanSingleton [IsDomain S] {π : S} (hπ : π ≠ 0) :
    (Ideal.span {π} : Ideal S) ≃ₗ[S] S
lemma

isPrincipal_of_linearEquiv

L438 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.isPrincipal_of_linearEquiv
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
section principal
variable {S : Type*} [CommRing S]
Lean source · statement
lemma isPrincipal_of_linearEquiv (P : Ideal S) (e : P ≃ₗ[S] S) : P.IsPrincipal
theorem

ufd_of_heightOne_principal

L452 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.ufd_of_heightOne_principal
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
Lean source · statement
theorem ufd_of_heightOne_principal (S : Type*) [CommRing S] [IsDomain S] [IsNoetherianRing S]
    (h : ∀ P : Ideal S, P.IsPrime → P ≠ ⊥ → P.height ≤ 1 → P.IsPrincipal) :
    UniqueFactorizationMonoid S
lemma

nonempty_linearEquiv_localization

L476 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.nonempty_linearEquiv_localization
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
section locallyPrincipal
variable {S : Type u} [CommRing S] [IsDomain S] (P : Ideal S) (hP0 : P ≠ ⊥)
  (hloc : ∀ (Q : Ideal S) [Q.IsPrime], (P.map (algebraMap S (Localization.AtPrime Q))).IsPrincipal)
include hP0 hloc
Lean source · statement
lemma nonempty_linearEquiv_localization (Q : Ideal S) [Q.IsPrime] :
    Nonempty ((P.map (algebraMap S (Localization.AtPrime Q)) : Ideal (Localization.AtPrime Q))
      ≃ₗ[Localization.AtPrime Q] Localization.AtPrime Q)
lemma

projective

L492 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.projective
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
section locallyPrincipal
variable {S : Type u} [CommRing S] [IsDomain S] (P : Ideal S) (hP0 : P ≠ ⊥)
  (hloc : ∀ (Q : Ideal S) [Q.IsPrime], (P.map (algebraMap S (Localization.AtPrime Q))).IsPrincipal)
include hP0 hloc
Lean source · statement
lemma projective [IsNoetherianRing S] : Module.Projective S P
lemma

invertible

L503 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.invertible
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
section locallyPrincipal
variable {S : Type u} [CommRing S] [IsDomain S] (P : Ideal S) (hP0 : P ≠ ⊥)
  (hloc : ∀ (Q : Ideal S) [Q.IsPrime], (P.map (algebraMap S (Localization.AtPrime Q))).IsPrincipal)
include hP0 hloc
Lean source · statement
lemma invertible [IsNoetherianRing S] : Module.Invertible S P
lemma

isPrincipal_of_isStablyFree

L524 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.isPrincipal_of_isStablyFree
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
section locallyPrincipal
variable {S : Type u} [CommRing S] [IsDomain S] (P : Ideal S) (hP0 : P ≠ ⊥)
  (hloc : ∀ (Q : Ideal S) [Q.IsPrime], (P.map (algebraMap S (Localization.AtPrime Q))).IsPrincipal)
include hP0 hloc
Lean source · statement
lemma isPrincipal_of_isStablyFree [IsNoetherianRing S] [Module.IsStablyFree S P] : P.IsPrincipal
lemma

isRegularRing_localization

L537 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.isRegularRing_localization
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
section regular
variable {R : Type u} [CommRing R]
Lean source · statement
lemma isRegularRing_localization [IsRegularRing R] (M : Submonoid R) :
    IsRegularRing (Localization M)
lemma

exists_prime_mem_maximalIdeal

L548 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.exists_prime_mem_maximalIdeal
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
section induction
Lean source · statement
lemma exists_prime_mem_maximalIdeal (R : Type u) [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    (h : maximalIdeal R ≠ ⊥) : ∃ x ∈ maximalIdeal R, x ∉ maximalIdeal R ^ 2 ∧ Prime x
theorem

ufd_of_ringKrullDim_le

L575 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing.P2mAB.ufd_of_ringKrullDim_le
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
namespace P2mAB
section induction
Lean source · statement
theorem ufd_of_ringKrullDim_le (d : ℕ) :
    ∀ (R : Type u) [CommRing R] [IsLocalRing R] [IsRegularRing R],
      ringKrullDim R ≤ d → UniqueFactorizationMonoid R
theorem

uniqueFactorizationMonoid_of_isLocalRing

L676 ↗
IsRegularRing.uniqueFactorizationMonoid_of_isLocalRing
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
open IsLocalRing RingTheory.Sequence
open scoped TensorProduct
universe u v w
open P2mAB IsLocalRing in
Lean source · statement
theorem _root_.IsRegularRing.uniqueFactorizationMonoid_of_isLocalRing
    (R : Type*) [CommRing R] [IsDomain R] [IsLocalRing R] [IsRegularRing R] :
    UniqueFactorizationMonoid R

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.