Module

IsLocalRing_mk_comp_algebraMap_surjective_of_maximalIdeal_le.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_mk_comp_algebraMap_surjective_of_maximalIdeal_le

4 declarations indexed from sourceView source ↗

Module documentation

Is Local Ring mk comp algebra Map surjective of maximal Ideal le

Imports4

Mathlib.RingTheory.AdicCompletion.Functoriality
Mathlib.RingTheory.AdicCompletion.Noetherian
Mathlib.RingTheory.Nakayama
Mathlib.RingTheory.Ideal.Quotient.Noetherian

Imported by1

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.All

theorem

map_maximalIdeal_le

L38 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_mk_comp_algebraMap_surjective_of_maximalIdeal_le.M4cP4PERT.map_maximalIdeal_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_mk_comp_algebraMap_surjective_of_maximalIdeal_le
universe u v
namespace M4cP4PERT
open IsLocalRing
section Local
variable {𝒪 : Type u} {A : Type v} [CommRing 𝒪] [IsLocalRing 𝒪] [CommRing A] [Algebra 𝒪 A]
  [IsLocalRing A]

Lean source · statement

theorem map_maximalIdeal_le
    (hres : Function.Surjective (⇑(Ideal.Quotient.mk (maximalIdeal A)) ∘ ⇑(algebraMap 𝒪 A))) :
    (maximalIdeal 𝒪).map (algebraMap 𝒪 A) ≤ maximalIdeal A

theorem

surjective_of_maximalIdeal_le_sup

L58 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_mk_comp_algebraMap_surjective_of_maximalIdeal_le.M4cP4PERT.surjective_of_maximalIdeal_le_sup

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_mk_comp_algebraMap_surjective_of_maximalIdeal_le
universe u v
namespace M4cP4PERT
open IsLocalRing
section Main
variable {𝒪 : Type u} {A : Type v} [CommRing 𝒪] [IsLocalRing 𝒪] [IsPrecomplete (maximalIdeal 𝒪) 𝒪]
  [CommRing A] [Algebra 𝒪 A] [IsLocalRing A] [IsNoetherianRing A]

Lean source · statement

theorem surjective_of_maximalIdeal_le_sup {J : Ideal A} (hJ : J ≤ maximalIdeal A)
    (hres : Function.Surjective (⇑(Ideal.Quotient.mk (maximalIdeal A)) ∘ ⇑(algebraMap 𝒪 A)))
    (hle : maximalIdeal A ≤ J ⊔ (maximalIdeal 𝒪).map (algebraMap 𝒪 A)) :
    Function.Surjective (⇑(Ideal.Quotient.mk J) ∘ ⇑(algebraMap 𝒪 A))

theorem

main

L99 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_mk_comp_algebraMap_surjective_of_maximalIdeal_le.M4cP4PERT.main

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_mk_comp_algebraMap_surjective_of_maximalIdeal_le
universe u v
namespace M4cP4PERT
open IsLocalRing
section Main
variable {𝒪 : Type u} {A : Type v} [CommRing 𝒪] [IsLocalRing 𝒪] [IsPrecomplete (maximalIdeal 𝒪) 𝒪]
  [CommRing A] [Algebra 𝒪 A] [IsLocalRing A] [IsNoetherianRing A]

Lean source · statement

theorem main
    (hres : Function.Surjective (⇑(residue A) ∘ ⇑(algebraMap 𝒪 A)))
    {J : Ideal A}
    (hle : maximalIdeal A ≤ J ⊔ maximalIdeal A ^ 2 ⊔ (maximalIdeal 𝒪).map (algebraMap 𝒪 A)) :
    Function.Surjective (⇑(Ideal.Quotient.mk J) ∘ ⇑(algebraMap 𝒪 A))

theorem

mk_comp_algebraMap_surjective_of_maximalIdeal_le

L124 ↗

IsLocalRing.mk_comp_algebraMap_surjective_of_maximalIdeal_le

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_mk_comp_algebraMap_surjective_of_maximalIdeal_le
universe u v

Lean source · statement

theorem _root_.IsLocalRing.mk_comp_algebraMap_surjective_of_maximalIdeal_le
    {𝒪 : Type u} {A : Type v} [CommRing 𝒪] [IsLocalRing 𝒪] [IsPrecomplete (IsLocalRing.maximalIdeal
      𝒪) 𝒪]
    [CommRing A] [Algebra 𝒪 A] [IsLocalRing A] [IsNoetherianRing A]
    (hres : Function.Surjective (⇑(IsLocalRing.residue A) ∘ ⇑(algebraMap 𝒪 A)))
    {J : Ideal A}
    (hle : IsLocalRing.maximalIdeal A ≤
      J ⊔ IsLocalRing.maximalIdeal A ^ 2 ⊔ (IsLocalRing.maximalIdeal 𝒪).map (algebraMap 𝒪 A)) :
    Function.Surjective (⇑(Ideal.Quotient.mk J) ∘ ⇑(algebraMap 𝒪 A))

Module documentation

Is Local Ring mk comp algebra Map surjective of maximal Ideal le

Declarations

map_maximalIdeal_le

surjective_of_maximalIdeal_le_sup

main

mk_comp_algebraMap_surjective_of_maximalIdeal_le