Module

ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup

7 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring is Alg Closed completion of mul Archimedean value Group

Imports6

Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.RingTheory.Valuation.RankOne
Mathlib.Topology.Algebra.Valued.WithVal
Mathlib.Topology.Algebra.Valued.NormedValued
Mathlib.Analysis.Normed.Field.Dense
Mathlib.Tactic.Push

Imported by1

Nyll.AlgebraicCurves.Valuations.All

theorem

mulArchimedean_valueGroup₀

L37 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup.P2mR1W0kur.mulArchimedean_valueGroup₀

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup
open MonoidWithZeroHom
namespace P2mR1W0kur
section Kurschak
variable {K : Type*} [Field K] (A : ValuationSubring K)

Lean source · statement

theorem mulArchimedean_valueGroup₀ {L Γ₀ : Type*} [Field L] [LinearOrderedCommGroupWithZero Γ₀]
    [MulArchimedean Γ₀] (v : Valuation L Γ₀) : MulArchimedean (ValueGroup₀ (.ofClass v))

def

rankOneOfMulArchimedean

L44 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup.P2mR1W0kur.rankOneOfMulArchimedean

Documentation

The rank-one structure supplied by a nontrivial valuation with Archimedean value group.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup
open MonoidWithZeroHom
namespace P2mR1W0kur
section Kurschak
variable {K : Type*} [Field K] (A : ValuationSubring K)

Lean source · statement

def rankOneOfMulArchimedean {L Γ₀ : Type*} [Field L]
    [LinearOrderedCommGroupWithZero Γ₀] [MulArchimedean Γ₀] (v : Valuation L Γ₀)
    [v.IsNontrivial] : v.RankOne

theorem

isNontrivial_valuation

L53 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup.P2mR1W0kur.isNontrivial_valuation

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup
open MonoidWithZeroHom
namespace P2mR1W0kur
section Kurschak
variable {K : Type*} [Field K] (A : ValuationSubring K)

Lean source · statement

theorem isNontrivial_valuation (hA : A ≠ ⊤) : A.valuation.IsNontrivial

theorem

isNontrivial_withVal

L65 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup.P2mR1W0kur.isNontrivial_withVal

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup
open MonoidWithZeroHom
namespace P2mR1W0kur
section Kurschak
variable {K : Type*} [Field K] (A : ValuationSubring K)

Lean source · statement

theorem isNontrivial_withVal (hA : A ≠ ⊤) :
    (Valued.v (R := WithVal A.valuation)).IsNontrivial

theorem

isNontrivial_completion

L70 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup.P2mR1W0kur.isNontrivial_completion

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup
open MonoidWithZeroHom
namespace P2mR1W0kur
section Kurschak
variable {K : Type*} [Field K] (A : ValuationSubring K)

Lean source · statement

theorem isNontrivial_completion (hA : A ≠ ⊤) :
    (Valued.v (R := A.valuation.Completion)).IsNontrivial

theorem

isAlgClosed_completion

L77 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup.P2mR1W0kur.isAlgClosed_completion

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup
open MonoidWithZeroHom
namespace P2mR1W0kur
section Kurschak
variable {K : Type*} [Field K] (A : ValuationSubring K)

Lean source · statement

theorem isAlgClosed_completion [IsAlgClosed K] [CharZero K] [MulArchimedean A.ValueGroup]
    (hA : A ≠ ⊤) :
    IsAlgClosed A.valuation.Completion

theorem

isAlgClosed_completion_of_mulArchimedean_valueGroup

L98 ↗

ValuationSubring.isAlgClosed_completion_of_mulArchimedean_valueGroup

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup
open MonoidWithZeroHom

Lean source · statement

theorem _root_.ValuationSubring.isAlgClosed_completion_of_mulArchimedean_valueGroup
    {K : Type*} [Field K] [IsAlgClosed K] [CharZero K]
    (A : ValuationSubring K) [MulArchimedean A.ValueGroup] (hA : A ≠ ⊤) :
    IsAlgClosed A.valuation.Completion

Module documentation

Valuation Subring is Alg Closed completion of mul Archimedean value Group

Declarations

mulArchimedean_valueGroup₀

rankOneOfMulArchimedean

isNontrivial_valuation

isNontrivial_withVal

isNontrivial_completion

isAlgClosed_completion

isAlgClosed_completion_of_mulArchimedean_valueGroup