Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_exists_isLocalRing_adicCompletion_isAdicComplete_map_maximalIdeal_eq

theorem

exists_isLocalRing_adicCompletion_isAdicComplete_map_maximalIdeal_eq

IsLocalRing.exists_isLocalRing_adicCompletion_isAdicComplete_map_maximalIdeal_eq

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_isLocalRing_adicCompletion_isAdicComplete_map_maximalIdeal_eq
universe u
open AdicCompletion IsLocalRing in

Lean source · statement

theorem _root_.IsLocalRing.exists_isLocalRing_adicCompletion_isAdicComplete_map_maximalIdeal_eq
    (O : Type u) [CommRing O] [IsNoetherianRing O] [IsLocalRing O] :
    ∃ (_ : IsLocalRing (AdicCompletion (maximalIdeal O) O))
      (_ : IsLocalHom (algebraMap O (AdicCompletion (maximalIdeal O) O))),
      IsAdicComplete (maximalIdeal (AdicCompletion (maximalIdeal O) O)) (AdicCompletion
        (maximalIdeal O) O) ∧
      Ideal.map (algebraMap O (AdicCompletion (maximalIdeal O) O)) (maximalIdeal O) =
        maximalIdeal (AdicCompletion (maximalIdeal O) O) ∧
      ∀ x : AdicCompletion (maximalIdeal O) O, ∃ o : O,
        x - algebraMap O (AdicCompletion (maximalIdeal O) O) o ∈ maximalIdeal (AdicCompletion
          (maximalIdeal O) O)

IsLocalRing_exists_isLocalRing_adicCompletion_isAdicComplete_map_maximalIdeal_eq.lean

Module documentation

Is Local Ring exists is Local Ring adic Completion is Adic Complete map maximal Ideal eq

exists_isLocalRing_adicCompletion_isAdicComplete_map_maximalIdeal_eq

Module documentation

Is Local Ring exists is Local Ring adic Completion is Adic Complete map maximal Ideal eq

Declarations

exists_isLocalRing_adicCompletion_isAdicComplete_map_maximalIdeal_eq