NYLL
Module

IsLocalRing_comap_map_adicCompletion_eq.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_comap_map_adicCompletion_eq
2 declarations indexed from sourceView source ↗

Module documentation

Is Local Ring comap map adic Completion eq

Imports2
  • Mathlib.RingTheory.AdicCompletion.AsTensorProduct
  • Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Imported by1

Declarations

theorem

faithfullyFlat_adicCompletion

L28 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_comap_map_adicCompletion_eq.C4sol.faithfullyFlat_adicCompletion
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_comap_map_adicCompletion_eq
namespace C4sol
open IsLocalRing
Lean source · statement
theorem faithfullyFlat_adicCompletion (R : Type*) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
  :
    Module.FaithfullyFlat R (AdicCompletion (maximalIdeal R) R)
theorem

comap_map_adicCompletion_eq

L53 ↗
IsLocalRing.comap_map_adicCompletion_eq
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_comap_map_adicCompletion_eq
open IsLocalRing in
Lean source · statement
theorem _root_.IsLocalRing.comap_map_adicCompletion_eq
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (I : Ideal R) :
    (I.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R))).comap
      (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) = I

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