Module

Mathlib_RingTheory_RegularLocalRingFlatLocalAscent.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Mathlib_RingTheory_RegularLocalRingFlatLocalAscent

8 declarations indexed from sourceView source ↗

Module documentation

Mathlib Ring Theory Regular Local Ring Flat Local Ascent

Imports4

Imported by2

def

quotSpanSingletonEquivQuotSMulTop

L33 ↗

RegularFlatLocalAscent.quotSpanSingletonEquivQuotSMulTop

Documentation

The linear equivalence between quotienting by a principal ideal and by its scalar-multiple submodule.

Source context 5 commands

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

noncomputable section
open IsLocalRing RingTheory
open scoped Pointwise
namespace RegularFlatLocalAscent
universe u v

Lean source · statement

def quotSpanSingletonEquivQuotSMulTop {R : Type u} [CommRing R] (x : R) :
    (R ⧸ Ideal.span {x}) ≃ₗ[R ⧸ Ideal.span {x}] QuotSMulTop x R

theorem

exists_isWeaklyRegular_ofList_eq_maximalIdeal_aux

L39 ↗

RegularFlatLocalAscent.exists_isWeaklyRegular_ofList_eq_maximalIdeal_aux

Source context 5 commands

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

noncomputable section
open IsLocalRing RingTheory
open scoped Pointwise
namespace RegularFlatLocalAscent
universe u v

Lean source · statement

theorem exists_isWeaklyRegular_ofList_eq_maximalIdeal_aux :
    ∀ (n : ℕ) (R : Type u) [CommRing R] [IsRegularLocalRing R],
      (maximalIdeal R).spanFinrank = n →
      ∃ rs : List R, Ideal.ofList rs = maximalIdeal R ∧ rs.length = n ∧
        Sequence.IsWeaklyRegular R rs

theorem

exists_isWeaklyRegular_ofList_eq_maximalIdeal

L130 ↗

RegularFlatLocalAscent.exists_isWeaklyRegular_ofList_eq_maximalIdeal

Source context 5 commands

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

noncomputable section
open IsLocalRing RingTheory
open scoped Pointwise
namespace RegularFlatLocalAscent
universe u v

Lean source · statement

theorem exists_isWeaklyRegular_ofList_eq_maximalIdeal (R : Type u) [CommRing R]
    [IsRegularLocalRing R] :
    ∃ rs : List R, Ideal.ofList rs = maximalIdeal R ∧
      rs.length = (maximalIdeal R).spanFinrank ∧ Sequence.IsWeaklyRegular R rs

theorem

exists_isRegular_ofList_eq_maximalIdeal

L136 ↗

RegularFlatLocalAscent.exists_isRegular_ofList_eq_maximalIdeal

Source context 5 commands

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

noncomputable section
open IsLocalRing RingTheory
open scoped Pointwise
namespace RegularFlatLocalAscent
universe u v

Lean source · statement

theorem exists_isRegular_ofList_eq_maximalIdeal (R : Type u) [CommRing R]
    [IsRegularLocalRing R] :
    ∃ rs : List R, Ideal.ofList rs = maximalIdeal R ∧
      rs.length = (maximalIdeal R).spanFinrank ∧ Sequence.IsRegular R rs

theorem

isRegularLocalRing_of_flat_of_isRegularLocalRing_quotient

L147 ↗

RegularFlatLocalAscent.isRegularLocalRing_of_flat_of_isRegularLocalRing_quotient

Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory
open scoped Pointwise
namespace RegularFlatLocalAscent
universe u v
open RegularLocalRingQuotientAscent in

Lean source · statement

theorem isRegularLocalRing_of_flat_of_isRegularLocalRing_quotient
    (R : Type u) (S : Type v) [CommRing R] [IsRegularLocalRing R] [CommRing S] [Algebra R S]
    [Module.Flat R S] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [IsNoetherianRing S]
    (hfiber : IsRegularLocalRing (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))) :
    IsRegularLocalRing S

theorem

flatLocalAscent_forall

L171 ↗

RegularFlatLocalAscent.flatLocalAscent_forall

Source context 5 commands

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

noncomputable section
open IsLocalRing RingTheory
open scoped Pointwise
namespace RegularFlatLocalAscent
universe u v

Lean source · statement

theorem flatLocalAscent_forall :
    ∀ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [IsRegularLocalRing R]
      [Algebra R S] [Module.Flat R S] [IsLocalRing S] [IsLocalHom (algebraMap R S)]
      [IsNoetherianRing S],
      IsRegularLocalRing (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) →
      IsRegularLocalRing S

theorem

gate_flat_ascent_runs_at_identity

L180 ↗

RegularFlatLocalAscent.gate_flat_ascent_runs_at_identity

Source context 5 commands

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

noncomputable section
open IsLocalRing RingTheory
open scoped Pointwise
namespace RegularFlatLocalAscent
universe u v

Lean source · statement

theorem gate_flat_ascent_runs_at_identity (p : ℕ) [Fact p.Prime] :
    IsRegularLocalRing ℤ_[p]

theorem

not_forall_ascent_dropping_flat

L195 ↗

RegularFlatLocalAscent.not_forall_ascent_dropping_flat

Source context 5 commands

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

noncomputable section
open IsLocalRing RingTheory
open scoped Pointwise
namespace RegularFlatLocalAscent
universe u v

Lean source · statement

theorem not_forall_ascent_dropping_flat :
    ¬ ∀ (R S : Type) [CommRing R] [CommRing S] [IsRegularLocalRing R] [Algebra R S]
        [IsLocalRing S] [IsLocalHom (algebraMap R S)] [IsNoetherianRing S],
        IsRegularLocalRing (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) →
        IsRegularLocalRing S

Module documentation

Mathlib Ring Theory Regular Local Ring Flat Local Ascent

Declarations