NYLL
Module

Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff.lean

Nyll.AlgebraicCurves.Places.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
12 declarations indexed from sourceView source ↗

Module documentation

Place exists valuation Subring alg Hom apply eq forall mem iff

Imports6
Imported by1

Declarations

theorem

exists_valuationSubring_over

L52 ↗
AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff.AlgebraicCurve.PlaceRealisation.exists_valuationSubring_over
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceRealisation
open IsLocalRing Polynomial
open scoped IntermediateField Pointwise
section Chevalley
variable {Ω : Type*} [Field Ω] {Ω' : Type*} [Field Ω'] [Algebra Ω Ω']
Lean source · statement
theorem exists_valuationSubring_over (A : ValuationSubring Ω) :
    ∃ O : ValuationSubring Ω', ∀ a : Ω, algebraMap Ω Ω' a ∈ O ↔ a ∈ A
theorem

mem_nonunits_of_over

L75 ↗
AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff.AlgebraicCurve.PlaceRealisation.mem_nonunits_of_over
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceRealisation
open IsLocalRing Polynomial
open scoped IntermediateField Pointwise
section Chevalley
variable {Ω : Type*} [Field Ω] {Ω' : Type*} [Field Ω'] [Algebra Ω Ω']
Lean source · statement
theorem mem_nonunits_of_over {A : ValuationSubring Ω} {O : ValuationSubring Ω'}
    (hO : ∀ a : Ω, algebraMap Ω Ω' a ∈ O ↔ a ∈ A) {a : Ω} (ha : a ∈ A.nonunits) :
    algebraMap Ω Ω' a ∈ O.nonunits
theorem

vs_ne_zero_of_notMem_nonunits

L89 ↗
AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff.AlgebraicCurve.PlaceRealisation.vs_ne_zero_of_notMem_nonunits
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceRealisation
open IsLocalRing Polynomial
open scoped IntermediateField Pointwise
section Nonunits
variable {L : Type*} [Field L] (A : ValuationSubring L)
Lean source · statement
theorem vs_ne_zero_of_notMem_nonunits {a : L} (ha : a ∉ A.nonunits) : a ≠ 0
theorem

vs_inv_mem_of_notMem_nonunits

L92 ↗
AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff.AlgebraicCurve.PlaceRealisation.vs_inv_mem_of_notMem_nonunits
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceRealisation
open IsLocalRing Polynomial
open scoped IntermediateField Pointwise
section Nonunits
variable {L : Type*} [Field L] (A : ValuationSubring L)
Lean source · statement
theorem vs_inv_mem_of_notMem_nonunits {a : L} (ha : a ∉ A.nonunits) : a⁻¹ ∈ A
theorem

vs_add_notMem_nonunits

L97 ↗
AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff.AlgebraicCurve.PlaceRealisation.vs_add_notMem_nonunits
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceRealisation
open IsLocalRing Polynomial
open scoped IntermediateField Pointwise
section Nonunits
variable {L : Type*} [Field L] (A : ValuationSubring L)
Lean source · statement
theorem vs_add_notMem_nonunits {a b : L} (ha : a ∉ A.nonunits) (hb : b ∈ A.nonunits) :
    a + b ∉ A.nonunits
theorem

vs_mul_mem_nonunits

L101 ↗
AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff.AlgebraicCurve.PlaceRealisation.vs_mul_mem_nonunits
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceRealisation
open IsLocalRing Polynomial
open scoped IntermediateField Pointwise
section Nonunits
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable {A} in
Lean source · statement
theorem vs_mul_mem_nonunits {a x : L} (ha : a ∈ A) (hx : x ∈ A.nonunits) :
    a * x ∈ A.nonunits
theorem

vs_one_notMem_nonunits

L110 ↗
AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff.AlgebraicCurve.PlaceRealisation.vs_one_notMem_nonunits
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceRealisation
open IsLocalRing Polynomial
open scoped IntermediateField Pointwise
section Nonunits
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable {A} in
variable {A} in
Lean source · statement
theorem vs_one_notMem_nonunits : (1 : L) ∉ A.nonunits
theorem

mem_iff_mem_of_sub_mem_nonunits

L119 ↗
AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff.AlgebraicCurve.PlaceRealisation.mem_iff_mem_of_sub_mem_nonunits
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceRealisation
open IsLocalRing Polynomial
open scoped IntermediateField Pointwise
section RationalPlace
variable {L : Type*} [Field L] {M : Type*} [Field M] [Algebra L M]
Lean source · statement
theorem mem_iff_mem_of_sub_mem_nonunits (t : M) (ht : Transcendental L t) (j₀ : L)
    (V₁ V₂ : ValuationSubring M)
    (hL₁ : ∀ c : L, algebraMap L M c ∈ V₁) (hL₂ : ∀ c : L, algebraMap L M c ∈ V₂)
    (h₁ : t - algebraMap L M j₀ ∈ V₁.nonunits) (h₂ : t - algebraMap L M j₀ ∈ V₂.nonunits)
    (f : M) (hf : f ∈ L⟮t⟯) : f ∈ V₁ ↔ f ∈ V₂
theorem

exists_algHom_adjoin_simple

L220 ↗
AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff.AlgebraicCurve.PlaceRealisation.exists_algHom_adjoin_simple
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceRealisation
open IsLocalRing Polynomial
open scoped IntermediateField Pointwise
section Main
variable {K : Type*} [Field K] {M : Type*} [Field M] [Algebra K M]
Lean source · statement
theorem exists_algHom_adjoin_simple (t : M) (ht : Transcendental K t)
    {Ω' : Type*} [Field Ω'] [Algebra K Ω'] (j : Ω') (hj : Transcendental K j) :
    ∃ f₀ : K⟮t⟯ →ₐ[K] Ω', f₀ (IntermediateField.AdjoinSimple.gen K t) = j
theorem

mem_nonunits_of_ord_pos

L231 ↗
AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff.AlgebraicCurve.PlaceRealisation.mem_nonunits_of_ord_pos
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceRealisation
open IsLocalRing Polynomial
open scoped IntermediateField Pointwise
section Main
variable {K : Type*} [Field K] {M : Type*} [Field M] [Algebra K M]
Lean source · statement
theorem mem_nonunits_of_ord_pos {F : Type*} [Field F] [Algebra K F] (v : Place K F) {f : F}
    (h : 0 < v.ord f) : f ∈ v.toValuationSubring.nonunits
theorem

exists_valuationSubring_algHom

L250 ↗
AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff.AlgebraicCurve.PlaceRealisation.exists_valuationSubring_algHom
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceRealisation
open IsLocalRing Polynomial
open scoped IntermediateField Pointwise
section Main
variable {K : Type*} [Field K] {M : Type*} [Field M] [Algebra K M]
Lean source · statement
theorem exists_valuationSubring_algHom (t : M) (ht : Transcendental K t)
    [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
    (W₀ : Place K M) (j₀ : K) (hW₀ : t - algebraMap K M j₀ ∈ W₀.toValuationSubring.nonunits)
    {Ω : Type*} [Field Ω] [Algebra K Ω] (W : Place K Ω) (j : Ω) (hj : Transcendental K j)
    (hjW : j - algebraMap K Ω j₀ ∈ W.toValuationSubring.nonunits)
    (Ω' : Type*) [Field Ω'] [IsAlgClosed Ω'] [Algebra K Ω'] [Algebra Ω Ω']
    [IsScalarTower K Ω Ω'] :
    ∃ (O : ValuationSubring Ω') (ι : M →ₐ[K] Ω'),
      (∀ a : Ω, algebraMap Ω Ω' a ∈ O ↔ a ∈ W.toValuationSubring) ∧
      ι t = algebraMap Ω Ω' j ∧
      ∀ m : M, ι m ∈ O ↔ m ∈ W₀.toValuationSubring
theorem

exists_valuationSubring_algHom_apply_eq_forall_mem_iff

L350 ↗
AlgebraicCurve.Place.exists_valuationSubring_algHom_apply_eq_forall_mem_iff
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
universe u v w x in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_valuationSubring_algHom_apply_eq_forall_mem_iff
    {K : Type u} [Field K] {M : Type v} [Field M] [Algebra K M]
    (t : M) (ht : Transcendental K t) [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
    (W₀ : Place K M) (j₀ : K) (hW₀ : t - algebraMap K M j₀ ∈ W₀.toValuationSubring.nonunits)
    {Ω : Type w} [Field Ω] [Algebra K Ω] (W : Place K Ω) (j : Ω) (hj : Transcendental K j)
    (hjW : j - algebraMap K Ω j₀ ∈ W.toValuationSubring.nonunits)
    (Ω' : Type x) [Field Ω'] [IsAlgClosed Ω'] [Algebra K Ω'] [Algebra Ω Ω']
    [IsScalarTower K Ω Ω'] :
    ∃ (O : ValuationSubring Ω') (ι : M →ₐ[K] Ω'),
      (∀ a : Ω, algebraMap Ω Ω' a ∈ O ↔ a ∈ W.toValuationSubring) ∧
      ι t = algebraMap Ω Ω' j ∧
      ∀ m : M, ι m ∈ O ↔ m ∈ W₀.toValuationSubring

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