NYLL
Module

AlgHom_eq_of_forall_restrictAlong_eq_of_charZero.lean

Nyll.AlgebraicCurves.Geometry.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero
9 declarations indexed from sourceView source ↗

Module documentation

Alg Hom eq of forall restrict Along eq of char Zero

Imports8
Imported by1

Declarations

theorem

ord_nonneg_of_mem

L51 ↗
AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero.RigidEmb.ord_nonneg_of_mem
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
open scoped IntermediateField
namespace RigidEmb
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_nonneg_of_mem (v : Place K F) {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L67 ↗
AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero.RigidEmb.mem_of_ord_nonneg
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
open scoped IntermediateField
namespace RigidEmb
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mem_of_ord_nonneg (v : Place K F) {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring
theorem

ord_pos_of_mem_nonunits

L75 ↗
AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero.RigidEmb.ord_pos_of_mem_nonunits
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
open scoped IntermediateField
namespace RigidEmb
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_pos_of_mem_nonunits (v : Place K F) {f : F} (hf0 : f ≠ 0)
    (hf : f ∈ v.toValuationSubring.nonunits) : 0 < v.ord f
theorem

ord_algebraMap

L90 ↗
AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero.RigidEmb.ord_algebraMap
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
open scoped IntermediateField
namespace RigidEmb
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_algebraMap (v : Place K F) (c : K) : v.ord (algebraMap K F c) = 0
theorem

ord_sub_pos

L99 ↗
AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero.RigidEmb.ord_sub_pos
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
open scoped IntermediateField
namespace RigidEmb
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_sub_pos (v : Place K F) {f g : F} (hf0 : f ≠ 0) (hg0 : g ≠ 0) (hfg : f - g ≠ 0)
    (hf : 0 < v.ord f) (hg : 0 < v.ord g) : 0 < v.ord (f - g)
theorem

transcendental_of_not_mem_range

L106 ↗
AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero.RigidEmb.transcendental_of_not_mem_range
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
open scoped IntermediateField
namespace RigidEmb
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem transcendental_of_not_mem_range [IsAlgClosed K] {x : F} (hx : x ∉ (algebraMap K F).range) :
    Transcendental K x
theorem

infinite_place

L114 ↗
AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero.RigidEmb.infinite_place
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
open scoped IntermediateField
namespace RigidEmb
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem infinite_place [IsAlgClosed K] [CharZero K] [IsCurveOver K F] [Algebra.EssFiniteType K F]
    {t : F} (ht : Transcendental K t) : Infinite (Place K F)
theorem

ramificationIndexAlong_pos

L142 ↗
AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero.RigidEmb.ramificationIndexAlong_pos
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
open scoped IntermediateField
namespace RigidEmb
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ramificationIndexAlong_pos {F' : Type*} [Field F'] [Algebra K F'] (φ : F →ₐ[K] F')
    (hφ : φ.toRingHom.IsIntegral) (w : Place K F') : 0 < Place.ramificationIndexAlong φ w
theorem

algHom_eq_of_forall_restrictAlong_eq_of_charZero

L152 ↗
AlgebraicCurve.algHom_eq_of_forall_restrictAlong_eq_of_charZero
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.AlgHom_eq_of_forall_restrictAlong_eq_of_charZero
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
open scoped IntermediateField
open RigidEmb in
Lean source · statement
theorem _root_.AlgebraicCurve.algHom_eq_of_forall_restrictAlong_eq_of_charZero
    (K : Type) [Field K] [IsAlgClosed K] [CharZero K]
    (F₀ F₁ : Type) [Field F₀] [Field F₁] [Algebra K F₀] [Algebra K F₁]
    [IsCurveOver K F₀] [Algebra.EssFiniteType K F₀] [IsCurveOver K F₁] [Algebra.EssFiniteType K F₁]
    (φ₁ φ₂ : F₀ →ₐ[K] F₁) (h₁ : φ₁.IsIntegral) (h₂ : φ₂.IsIntegral)
    (h : ∀ w : Place K F₁, w.restrictAlong φ₁ h₁ = w.restrictAlong φ₂ h₂) :
    φ₁ = φ₂

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