NYLL
Module

Place_isRegularAt_D_algebraMap_of_forall_algebraMap_mem_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Places.Place_isRegularAt_D_algebraMap_of_forall_algebraMap_mem_of_isAlgClosed
4 declarations indexed from sourceView source ↗

Module documentation

Place is Regular At D algebra Map of forall algebra Map mem of is Alg Closed

Imports4
Imported by3

Declarations

theorem

ord_nonneg_of_mem

L56 ↗
AlgebraicCurves.Places.Proofs.Place_isRegularAt_D_algebraMap_of_forall_algebraMap_mem_of_isAlgClosed.AlgebraicCurve.GenericPlaceB1.ord_nonneg_of_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_isRegularAt_D_algebraMap_of_forall_algebraMap_mem_of_isAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericPlaceB1
open _root_.AlgebraicCurve
variable {L E : Type*} [Field L] [Field E] [Algebra L E] (v : Place L E)
Lean source · statement
theorem ord_nonneg_of_mem {f : E} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L69 ↗
AlgebraicCurves.Places.Proofs.Place_isRegularAt_D_algebraMap_of_forall_algebraMap_mem_of_isAlgClosed.AlgebraicCurve.GenericPlaceB1.mem_of_ord_nonneg
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_isRegularAt_D_algebraMap_of_forall_algebraMap_mem_of_isAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericPlaceB1
open _root_.AlgebraicCurve
variable {L E : Type*} [Field L] [Field E] [Algebra L E] (v : Place L E)
Lean source · statement
theorem mem_of_ord_nonneg {f : E} (hf : f ≠ 0) (h : 0 ≤ v.ord f) : f ∈ v.toValuationSubring
theorem

ord_eq_zero_of_mem_of_inv_mem

L75 ↗
AlgebraicCurves.Places.Proofs.Place_isRegularAt_D_algebraMap_of_forall_algebraMap_mem_of_isAlgClosed.AlgebraicCurve.GenericPlaceB1.ord_eq_zero_of_mem_of_inv_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_isRegularAt_D_algebraMap_of_forall_algebraMap_mem_of_isAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericPlaceB1
open _root_.AlgebraicCurve
variable {L E : Type*} [Field L] [Field E] [Algebra L E] (v : Place L E)
Lean source · statement
theorem ord_eq_zero_of_mem_of_inv_mem {f : E} (h1 : f ∈ v.toValuationSubring) (h2 : f⁻¹ ∈
  v.toValuationSubring) :
    v.ord f = 0
theorem

isRegularAt_D_algebraMap_of_forall_algebraMap_mem_of_isAlgClosed

L86 ↗
AlgebraicCurve.Place.isRegularAt_D_algebraMap_of_forall_algebraMap_mem_of_isAlgClosed
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_isRegularAt_D_algebraMap_of_forall_algebraMap_mem_of_isAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
open _root_.AlgebraicCurve AlgebraicCurve AlgebraicCurve.GenericPlaceB1 KaehlerDifferential in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.isRegularAt_D_algebraMap_of_forall_algebraMap_mem_of_isAlgClosed
    (K F K' F' : Type*)
    [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
    [IsAlgClosed K] [IsAlgClosed K'] [IsCurveOver K F] [IsCurveOver K' F']
    [Algebra.EssFiniteType K' F']
    (_hsep : ∃ x₀ : F, Transcendental K x₀ ∧ FiniteDimensional (IntermediateField.adjoin K ({x₀} :
      Set F)) F ∧
      Algebra.IsSeparable (IntermediateField.adjoin K ({x₀} : Set F)) F)
    (_hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    (_hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    (w : Place K' F') (hw : ∀ f : F, algebraMap F F' f ∈ w.toValuationSubring) (x : F) :
    w.IsRegularAt (KaehlerDifferential.D K' F' (algebraMap F F' x))

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