NYLL
Module

IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_of_isAlgClosed.lean

Nyll.AlgebraicCurves.FunctionFields.IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_of_isAlgClosed
6 declarations indexed from sourceView source ↗

Module documentation

Is Regular At map of forall is Regular At of constant Field Extension of is Alg Closed

Imports7
Imported by1

Declarations

theorem

ord_nonneg_of_mem

L60 ↗
AlgebraicCurves.FunctionFields.Proofs.IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.PolarBC.ord_nonneg_of_mem
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs
namespace IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_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 PolarBC
open _root_.AlgebraicCurve
section Ord
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

L73 ↗
AlgebraicCurves.FunctionFields.Proofs.IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.PolarBC.mem_of_ord_nonneg
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs
namespace IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_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 PolarBC
open _root_.AlgebraicCurve
section Ord
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

mem_of_ord_nonneg'

L79 ↗
AlgebraicCurves.FunctionFields.Proofs.IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.PolarBC.mem_of_ord_nonneg'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs
namespace IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_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 PolarBC
open _root_.AlgebraicCurve
section Ord
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} (h : 0 ≤ v.ord f) : f ∈ v.toValuationSubring
theorem

map_smul_D

L93 ↗
AlgebraicCurves.FunctionFields.Proofs.IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.PolarBC.map_smul_D
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs
namespace IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_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 PolarBC
open _root_.AlgebraicCurve
section CaseA
variable {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']
    [SMulCommClass K' F F']
Lean source · statement
theorem map_smul_D (f g : F) :
    KaehlerDifferential.map K K' F F' (f • D K F g) = algebraMap F F' f • D K' F' (algebraMap F F'
      g)
theorem

caseA

L101 ↗
AlgebraicCurves.FunctionFields.Proofs.IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_of_isAlgClosed.AlgebraicCurve.PolarBC.caseA
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs
namespace IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_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 PolarBC
open _root_.AlgebraicCurve
section CaseA
variable {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']
    [SMulCommClass K' F F']
variable [IsAlgClosed K'] [IsCurveOver K' F'] [Algebra.EssFiniteType K' F']
Lean source · statement
theorem caseA (v : Place K F) (w : Place K' F')
    (hmem : ∀ f : F, f ∈ v.toValuationSubring ↔ algebraMap F F' f ∈ w.toValuationSubring)
    (hord : ∀ f : F, w.ord (algebraMap F F' f) = v.ord f) (ω : Ω[F⁄K]) :
    (v.IsRegularAt ω → w.IsRegularAt (KaehlerDifferential.map K K' F F' ω)) ∧
      (v.HasSimplePoleAt ω → w.HasSimplePoleAt (KaehlerDifferential.map K K' F F' ω))
theorem

isRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_of_isAlgClosed

L145 ↗
AlgebraicCurve.isRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_of_isAlgClosed
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurve
open _root_.KaehlerDifferential in
open _root_.AlgebraicCurves.FunctionFields.Proofs in
open IsRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_of_isAlgClosed in
open AlgebraicCurve.PolarBC in
Lean source · statement
theorem isRegularAt_map_of_forall_isRegularAt_of_constantFieldExtension_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']
      [SMulCommClass K' F F']
    [IsAlgClosed K] [IsAlgClosed K'] [AlgebraicCurve.IsCurveOver K F] [AlgebraicCurve.IsCurveOver
      K' F']
    [Algebra.EssFiniteType K F] [Algebra.EssFiniteType K' F']
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (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')) = ⊤)
    (S : Set (AlgebraicCurve.Place K F))
    (ω : Ω[F⁄K]) (hω : ∀ v : AlgebraicCurve.Place K F, v ∉ S → v.IsRegularAt ω) :
    ∀ w : AlgebraicCurve.Place K' F',
      w ∉ {w : AlgebraicCurve.Place K' F' | ∃ v ∈ S, w.toValuationSubring.comap (algebraMap F F') =
        v.toValuationSubring} →
        w.IsRegularAt (KaehlerDifferential.map K K' F F' ω)

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