Module

IsLocalization_AtPrime_exists_ringEquiv_adicCompletion_maximalIdeal.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalization_AtPrime_exists_ringEquiv_adicCompletion_maximalIdeal

3 declarations indexed from sourceView source ↗

Module documentation

Is Localization At Prime exists ring Equiv adic Completion maximal Ideal

Imports2

Mathlib.RingTheory.AdicCompletion.Algebra
Mathlib.RingTheory.Localization.AtPrime.Basic

Imported by1

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.All

theorem

factorPow_evalₐ

L29 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalization_AtPrime_exists_ringEquiv_adicCompletion_maximalIdeal.L1BAdic.factorPow_evalₐ

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalization_AtPrime_exists_ringEquiv_adicCompletion_maximalIdeal
universe u v
namespace L1BAdic

Lean source · statement

theorem factorPow_evalₐ {S : Type u} [CommRing S] (J : Ideal S) {m n : ℕ} (hle : m ≤ n) (z :
  AdicCompletion J S) :
    Ideal.Quotient.factorPow J hle (AdicCompletion.evalₐ J n z) = AdicCompletion.evalₐ J m z

theorem

factorPow_evalₐ'

L39 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalization_AtPrime_exists_ringEquiv_adicCompletion_maximalIdeal.L1BAdic.factorPow_evalₐ'

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalization_AtPrime_exists_ringEquiv_adicCompletion_maximalIdeal
universe u v
namespace L1BAdic

Lean source · statement

theorem factorPow_evalₐ' {S : Type v} [CommRing S] (J : Ideal S) {m n : ℕ} (hle : m ≤ n) (z :
  AdicCompletion J S) :
    Ideal.Quotient.factorPow J hle (AdicCompletion.evalₐ J n z) = AdicCompletion.evalₐ J m z

theorem

exists_ringEquiv_adicCompletion_maximalIdeal

L51 ↗

IsLocalization.AtPrime.exists_ringEquiv_adicCompletion_maximalIdeal

Source context 4 commands

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

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

Lean source · statement

theorem _root_.IsLocalization.AtPrime.exists_ringEquiv_adicCompletion_maximalIdeal
    {B : Type u} [CommRing B] (𝔪 : Ideal B) [𝔪.IsMaximal]
    (O : Type v) [CommRing O] [IsLocalRing O] [Algebra B O] [IsLocalization.AtPrime O 𝔪] :
    ∃ ê : AdicCompletion 𝔪 B ≃+* AdicCompletion (IsLocalRing.maximalIdeal O) O,
      ∀ b : B, ê (algebraMap B (AdicCompletion 𝔪 B) b) =
        algebraMap O (AdicCompletion (IsLocalRing.maximalIdeal O) O) (algebraMap B O b)

Module documentation

Is Localization At Prime exists ring Equiv adic Completion maximal Ideal

Declarations

factorPow_evalₐ

factorPow_evalₐ'

exists_ringEquiv_adicCompletion_maximalIdeal