Module

IsRegularLocalRing_quotient_span_singleton_map_of_leftInverse_of_irreducible.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsRegularLocalRing_quotient_span_singleton_map_of_leftInverse_of_irreducible

3 declarations indexed from sourceView source ↗

Module documentation

Is Regular Local Ring quotient span singleton map of left Inverse of irreducible

Imports2

Imported by2

theorem

map_maximalIdeal_le_of_surjective

L31 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_quotient_span_singleton_map_of_leftInverse_of_irreducible.SecSmooth.map_maximalIdeal_le_of_surjective

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_quotient_span_singleton_map_of_leftInverse_of_irreducible
open IsLocalRing
namespace SecSmooth
open IsLocalRing

Lean source · statement

theorem map_maximalIdeal_le_of_surjective {R A : Type*} [CommRing R] [IsLocalRing R] [CommRing A]
  [IsLocalRing A]
    (s : R →+* A) (hs : Function.Surjective s) : (maximalIdeal R).map s ≤ maximalIdeal A

theorem

map_irreducible_notMem_maximalIdeal_sq

L38 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_quotient_span_singleton_map_of_leftInverse_of_irreducible.SecSmooth.map_irreducible_notMem_maximalIdeal_sq

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_quotient_span_singleton_map_of_leftInverse_of_irreducible
open IsLocalRing
namespace SecSmooth
open IsLocalRing

Lean source · statement

theorem map_irreducible_notMem_maximalIdeal_sq {R A : Type*} [CommRing R] [IsLocalRing R] [CommRing
  A] [IsDomain A]
    [IsDiscreteValuationRing A] (i : A →+* R) (s : R →+* A) (hs : Function.Surjective s) (hsi :
      s.comp i = RingHom.id A)
    {ϖ : A} (hϖ : Irreducible ϖ) : i ϖ ∉ maximalIdeal R ^ 2

theorem

quotient_span_singleton_map_of_leftInverse_of_irreducible

L62 ↗

IsRegularLocalRing.quotient_span_singleton_map_of_leftInverse_of_irreducible

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_quotient_span_singleton_map_of_leftInverse_of_irreducible
open IsLocalRing

Lean source · statement

theorem _root_.IsRegularLocalRing.quotient_span_singleton_map_of_leftInverse_of_irreducible
    {R A : Type*} [CommRing R] [IsRegularLocalRing R] [CommRing A] [IsDomain A]
      [IsDiscreteValuationRing A]
    (i : A →+* R) (s : R →+* A) (hs : Function.Surjective s) (hsi : s.comp i = RingHom.id A)
    {ϖ : A} (hϖ : Irreducible ϖ) :
    ∃ _ : IsRegularLocalRing (R ⧸ Ideal.span {i ϖ}),
      (maximalIdeal (R ⧸ Ideal.span {i ϖ})).spanFinrank + 1 = (maximalIdeal R).spanFinrank ∧
        ringKrullDim (R ⧸ Ideal.span {i ϖ}) + 1 = ringKrullDim R

Module documentation

Is Regular Local Ring quotient span singleton map of left Inverse of irreducible

Declarations

map_maximalIdeal_le_of_surjective

map_irreducible_notMem_maximalIdeal_sq

quotient_span_singleton_map_of_leftInverse_of_irreducible