NYLL
Module

Place_exists_toValuationSubring_eq_comap.lean

Nyll.AlgebraicCurves.Places.Place_exists_toValuationSubring_eq_comap
21 declarations indexed from sourceView source ↗

Module documentation

Place exists to Valuation Subring eq comap

Imports4
Imported by1

Declarations

theorem

ord_nonneg_of_mem'

L42 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_mem' {f : F} (hf : f ∈
  v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg'

L59 ↗
AlgebraicCurve.Place.mem_of_ord_nonneg'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_of_ord_nonneg' {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord
  f) :
    f ∈ v.toValuationSubring
theorem

mem_iff_ord_nonneg'

L69 ↗
AlgebraicCurve.Place.mem_iff_ord_nonneg'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_iff_ord_nonneg' {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f
theorem

exists_ord_pos_mem'

L74 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap.AlgebraicCurve.Place.exists_ord_pos_mem'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem exists_ord_pos_mem' : ∃ f : F, f ≠ 0 ∧ 0 < v.ord f ∧ f ∈ v.toValuationSubring
theorem

algebraMap_ne_zero'

L88 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap.AlgebraicCurve.Place.algebraMap_ne_zero'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
Lean source · statement
theorem algebraMap_ne_zero' {f : F} (hf : f ≠ 0) : algebraMap F F' f ≠ 0
theorem

comap_algebraMap_ne_top'

L93 ↗
AlgebraicCurve.Place.comap_algebraMap_ne_top'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
Lean source · statement
theorem _root_.AlgebraicCurve.Place.comap_algebraMap_ne_top' [Algebra.IsIntegral F F'] :
    w.toValuationSubring.comap (algebraMap F F') ≠ ⊤
theorem

mem_comap_iff_ord_nonneg'

L111 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap.AlgebraicCurve.Place.mem_comap_iff_ord_nonneg'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
Lean source · statement
theorem mem_comap_iff_ord_nonneg' {f : F} (hf : f ≠ 0) :
    f ∈ w.toValuationSubring.comap (algebraMap F F') ↔
      0 ≤ w.ord (algebraMap F F' f)
theorem

isUnit_mk_comap_iff'

L118 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap.AlgebraicCurve.Place.isUnit_mk_comap_iff'
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
Lean source · statement
theorem isUnit_mk_comap_iff' {f : F} (hf : f ≠ 0)
    (hmem : f ∈ w.toValuationSubring.comap (algebraMap F F')) :
    IsUnit (⟨f, hmem⟩ : w.toValuationSubring.comap (algebraMap F F')) ↔
      w.ord (algebraMap F F' f) = 0
theorem

exists_ord_algebraMap_pos'

L143 ↗
AlgebraicCurve.Place.exists_ord_algebraMap_pos'
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_ord_algebraMap_pos' [Algebra.IsIntegral F F'] :
    ∃ f : F, f ≠ 0 ∧ 0 < w.ord (algebraMap F F' f)
def

ramificationIndex'

L159 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap.AlgebraicCurve.Place.ramificationIndex'
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
open _root_.AlgebraicCurve.Place
Lean source · statement
def ramificationIndex' (F : Type*) [Field F] [Algebra F F'] : ℕ
theorem

ramificationIndex'_le_ord

L162 ↗
AlgebraicCurve.Place.ramificationIndex'_le_ord
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ramificationIndex'_le_ord {f : F} (hf : f ≠ 0)
    (hpos : 0 < w.ord (algebraMap F F' f)) :
    (ramificationIndex' (F := F) w : ℤ) ≤ w.ord (algebraMap F F' f)
theorem

ramificationIndex'_set_nonempty

L174 ↗
AlgebraicCurve.Place.ramificationIndex'_set_nonempty
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable [Algebra.IsIntegral F F']
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ramificationIndex'_set_nonempty :
    {n : ℕ | 0 < n ∧ ∃ f : F, f ≠ 0 ∧ w.ord (algebraMap F F' f) = n}.Nonempty
theorem

ramificationIndex'_pos

L180 ↗
AlgebraicCurve.Place.ramificationIndex'_pos
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable [Algebra.IsIntegral F F']
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ramificationIndex'_pos : 0 < ramificationIndex' (F :=
  F) w
theorem

exists_ord_eq_ramificationIndex'

L185 ↗
AlgebraicCurve.Place.exists_ord_eq_ramificationIndex'
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable [Algebra.IsIntegral F F']
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_ord_eq_ramificationIndex' :
    ∃ f : F, f ≠ 0 ∧ w.ord (algebraMap F F' f) = ramificationIndex' (F := F) w
theorem

ramificationIndex'_dvd_ord

L190 ↗
AlgebraicCurve.Place.ramificationIndex'_dvd_ord
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable [Algebra.IsIntegral F F']
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ramificationIndex'_dvd_ord {f : F} (hf : f ≠ 0) :
    (ramificationIndex' (F := F) w : ℤ) ∣ w.ord (algebraMap F F' f)
theorem

irreducible_mk_comap'

L219 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap.AlgebraicCurve.Place.irreducible_mk_comap'
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable [Algebra.IsIntegral F F']
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem irreducible_mk_comap' {g : F} (hg0 : g ≠ 0)
    (hmem : g ∈ w.toValuationSubring.comap (algebraMap F F'))
    (hge : w.ord (algebraMap F F' g) = ramificationIndex' (F := F) w) :
    Irreducible (⟨g, hmem⟩ : w.toValuationSubring.comap (algebraMap F F'))
theorem

isPrincipalIdealRing_comap'

L250 ↗
AlgebraicCurve.Place.isPrincipalIdealRing_comap'
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable [Algebra.IsIntegral F F']
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.isPrincipalIdealRing_comap' :
    IsPrincipalIdealRing (w.toValuationSubring.comap (algebraMap F F'))
def

restrict'

L299 ↗
AlgebraicCurve.Place.restrict'
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable [Algebra.IsIntegral F F']
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section RestrictDef
variable [Algebra K F] [IsScalarTower K F F']
variable (F) in
Lean source · full declaration
def _root_.AlgebraicCurve.Place.restrict' : Place K F where
  toValuationSubring := w.toValuationSubring.comap (algebraMap F F')
  algebraMap_mem' a := by
    rw [ValuationSubring.mem_comap, ← IsScalarTower.algebraMap_apply]
    exact w.algebraMap_mem' a
  ne_top' := w.comap_algebraMap_ne_top'
  isPrincipalIdealRing' := w.isPrincipalIdealRing_comap'
theorem

ord_restrict'

L308 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap.AlgebraicCurve.Place.ord_restrict'
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable [Algebra.IsIntegral F F']
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section RestrictDef
variable [Algebra K F] [IsScalarTower K F F']
variable (F) in
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem ord_restrict' (f : F) :
    w.ord (algebraMap F F' f) = ramificationIndex' (F := F) w * (w.restrict' F).ord f
theorem

rowMain

L339 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap.AlgebraicCurve.Place.rowMain
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable [Algebra.IsIntegral F F']
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section RestrictDef
variable [Algebra K F] [IsScalarTower K F F']
variable (F) in
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem rowMain :
    ∃ v : Place K F, v.toValuationSubring = w.toValuationSubring.comap (algebraMap F F')
theorem

exists_toValuationSubring_eq_comap

L355 ↗
AlgebraicCurve.Place.exists_toValuationSubring_eq_comap
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_toValuationSubring_eq_comap {K F F' : Type*} [Field K]
  [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] (w : Place K F') :
    ∃ v : Place K F, v.toValuationSubring = w.toValuationSubring.comap (algebraMap F F')

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