Module

IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete.lean

Nyll.AlgebraicCurves.Valuations.IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete

10 declarations indexed from sourceView source ↗

Module documentation

Is Discrete Valuation Ring adic Completion is Domain is Discrete Valuation Ring is Adic

Complete

Imports1

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.AdicCompletionLocalRing

Imported by1

Nyll.AlgebraicCurves.Valuations.All

theorem

maximalIdeal_eq_span

L33 ↗

AlgebraicCurves.Valuations.Proofs.IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete.ADICDVRe133.maximalIdeal_eq_span

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete
universe u
open IsLocalRing
namespace ADICDVRe133
variable {C : Type u} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]

Lean source · statement

theorem maximalIdeal_eq_span (ϖ : C) (hϖ : Irreducible ϖ) :
    maximalIdeal (AdicCompletion (maximalIdeal C) C) =
      Ideal.span {algebraMap C (AdicCompletion (maximalIdeal C) C) ϖ}

theorem

maximalIdeal_pow_eq_span

L38 ↗

AlgebraicCurves.Valuations.Proofs.IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete.ADICDVRe133.maximalIdeal_pow_eq_span

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete
universe u
open IsLocalRing
namespace ADICDVRe133
variable {C : Type u} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]

Lean source · statement

theorem maximalIdeal_pow_eq_span (ϖ : C) (hϖ : Irreducible ϖ) (n : ℕ) :
    maximalIdeal (AdicCompletion (maximalIdeal C) C) ^ n =
      Ideal.span {algebraMap C (AdicCompletion (maximalIdeal C) C) ϖ ^ n}

theorem

eq_zero_of_forall_mem_pow

L43 ↗

AlgebraicCurves.Valuations.Proofs.IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete.ADICDVRe133.eq_zero_of_forall_mem_pow

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete
universe u
open IsLocalRing
namespace ADICDVRe133
variable {C : Type u} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]

Lean source · statement

theorem eq_zero_of_forall_mem_pow (x : AdicCompletion (maximalIdeal C) C)
    (h : ∀ n, x ∈ maximalIdeal (AdicCompletion (maximalIdeal C) C) ^ n) : x = 0

theorem

algebraMap_pow_ne_zero

L50 ↗

AlgebraicCurves.Valuations.Proofs.IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete.ADICDVRe133.algebraMap_pow_ne_zero

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete
universe u
open IsLocalRing
namespace ADICDVRe133
variable {C : Type u} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]

Lean source · statement

theorem algebraMap_pow_ne_zero (ϖ : C) (hϖ : Irreducible ϖ) (m : ℕ) :
    algebraMap C (AdicCompletion (maximalIdeal C) C) ϖ ^ m ≠ 0

theorem

exists_eq_unit_mul_pow

L64 ↗

AlgebraicCurves.Valuations.Proofs.IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete.ADICDVRe133.exists_eq_unit_mul_pow

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete
universe u
open IsLocalRing
namespace ADICDVRe133
variable {C : Type u} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]

Lean source · statement

theorem exists_eq_unit_mul_pow (ϖ : C) (hϖ : Irreducible ϖ) (x : AdicCompletion (maximalIdeal C) C)
  (hx : x ≠ 0) :
    ∃ (n : ℕ) (v : (AdicCompletion (maximalIdeal C) C)ˣ),
      x = (v : AdicCompletion (maximalIdeal C) C) * algebraMap C (AdicCompletion (maximalIdeal C)
        C) ϖ ^ n

theorem

isDomain

L100 ↗

AlgebraicCurves.Valuations.Proofs.IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete.ADICDVRe133.isDomain

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete
universe u
open IsLocalRing
namespace ADICDVRe133
variable {C : Type u} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]

Lean source · statement

theorem isDomain (ϖ : C) (hϖ : Irreducible ϖ) : IsDomain (AdicCompletion (maximalIdeal C) C)

theorem

irreducible_algebraMap

L116 ↗

AlgebraicCurves.Valuations.Proofs.IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete.ADICDVRe133.irreducible_algebraMap

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete
universe u
open IsLocalRing
namespace ADICDVRe133
variable {C : Type u} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]

Lean source · statement

theorem irreducible_algebraMap (ϖ : C) (hϖ : Irreducible ϖ) :
    Irreducible (algebraMap C (AdicCompletion (maximalIdeal C) C) ϖ)

theorem

isDiscreteValuationRing

L165 ↗

AlgebraicCurves.Valuations.Proofs.IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete.ADICDVRe133.isDiscreteValuationRing

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete
universe u
open IsLocalRing
namespace ADICDVRe133
variable {C : Type u} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]

Lean source · statement

theorem isDiscreteValuationRing (ϖ : C) (hϖ : Irreducible ϖ) :
    @IsDiscreteValuationRing (AdicCompletion (maximalIdeal C) C) _ (isDomain ϖ hϖ)

theorem

isAdicComplete_maximalIdeal

L173 ↗

AlgebraicCurves.Valuations.Proofs.IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete.ADICDVRe133.isAdicComplete_maximalIdeal

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete
universe u
open IsLocalRing
namespace ADICDVRe133
variable {C : Type u} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]

Lean source · statement

theorem isAdicComplete_maximalIdeal :
    IsAdicComplete (maximalIdeal (AdicCompletion (maximalIdeal C) C)) (AdicCompletion (maximalIdeal
      C) C)

theorem

adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete

L183 ↗

IsDiscreteValuationRing.adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete
universe u
open IsLocalRing
open ADICDVRe133 in

Lean source · statement

theorem
  _root_.IsDiscreteValuationRing.adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete
    (C : Type u) [CommRing C] [IsDomain C] [IsDiscreteValuationRing C] (ϖ : C) (hϖ : Irreducible ϖ)
      :
    ∃ (_ : IsDomain (AdicCompletion (IsLocalRing.maximalIdeal C) C))
      (_ : IsDiscreteValuationRing (AdicCompletion (IsLocalRing.maximalIdeal C) C))
      (_ : IsAdicComplete (IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal C)
        C)) (AdicCompletion (IsLocalRing.maximalIdeal C) C)),
      Irreducible (algebraMap C (AdicCompletion (IsLocalRing.maximalIdeal C) C) ϖ) ∧
      (∀ (n : ℕ) (c : C), algebraMap C (AdicCompletion (IsLocalRing.maximalIdeal C) C) c ∈
          Ideal.span {algebraMap C (AdicCompletion (IsLocalRing.maximalIdeal C) C) ϖ ^ n} → c ∈
            Ideal.span {ϖ ^ n}) ∧
      (∀ (n : ℕ) (w : AdicCompletion (IsLocalRing.maximalIdeal C) C), ∃ c : C,
          w - algebraMap C (AdicCompletion (IsLocalRing.maximalIdeal C) C) c ∈
            Ideal.span {algebraMap C (AdicCompletion (IsLocalRing.maximalIdeal C) C) ϖ ^ n})

Module documentation

Is Discrete Valuation Ring adic Completion is Domain is Discrete Valuation Ring is Adic

Declarations