NYLL
Module

Ideal_comap_map_adicCompletion_eq_of_isNoetherianRing.lean

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

Module documentation

Ideal comap map adic Completion eq of is Noetherian Ring

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

Declarations

theorem

faithfullyFlat_adicCompletion_maximalIdeal

L25 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_comap_map_adicCompletion_eq_of_isNoetherianRing.Ws34.faithfullyFlat_adicCompletion_maximalIdeal
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_comap_map_adicCompletion_eq_of_isNoetherianRing
Lean source · statement
theorem Ws34.faithfullyFlat_adicCompletion_maximalIdeal (S : Type*) [CommRing S] [IsNoetherianRing
  S]
    [IsLocalRing S] : Module.FaithfullyFlat S (AdicCompletion (IsLocalRing.maximalIdeal S) S)
theorem

comap_map_adicCompletion_eq_of_isNoetherianRing

L50 ↗
Ideal.comap_map_adicCompletion_eq_of_isNoetherianRing
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_comap_map_adicCompletion_eq_of_isNoetherianRing
Lean source · statement
theorem _root_.Ideal.comap_map_adicCompletion_eq_of_isNoetherianRing
    {S : Type*} [CommRing S] [IsNoetherianRing S] [IsLocalRing S] (𝔞 : Ideal S) :
    (𝔞.map (algebraMap S (AdicCompletion (IsLocalRing.maximalIdeal S) S))).comap
        (algebraMap S (AdicCompletion (IsLocalRing.maximalIdeal S) S)) = 𝔞

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