NYLL
Module

Divisor_pullbackAlong_liesOver_of_liesOver.lean

Nyll.AlgebraicCurves.Divisors.Divisor_pullbackAlong_liesOver_of_liesOver
3 declarations indexed from sourceView source ↗

Module documentation

Divisor pullback Along lies Over of lies Over

Imports4
Imported by2

Declarations

theorem

restrictAlong_toValuationSubring

L35 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pullbackAlong_liesOver_of_liesOver.AlgebraicCurve.A1Aux.restrictAlong_toValuationSubring
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pullbackAlong_liesOver_of_liesOver
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace A1Aux
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem restrictAlong_toValuationSubring (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (w : Place K F') :
    (w.restrictAlong φ hφ).toValuationSubring = w.toValuationSubring.comap φ.toRingHom
theorem

mem_restrictAlong_iff

L40 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pullbackAlong_liesOver_of_liesOver.AlgebraicCurve.A1Aux.mem_restrictAlong_iff
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pullbackAlong_liesOver_of_liesOver
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace A1Aux
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem mem_restrictAlong_iff (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (w : Place K F') (f : F) :
    f ∈ (w.restrictAlong φ hφ).toValuationSubring ↔ φ f ∈ w.toValuationSubring
theorem

pullbackAlong_liesOver_of_liesOver

L47 ↗
AlgebraicCurve.Divisor.pullbackAlong_liesOver_of_liesOver
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pullbackAlong_liesOver_of_liesOver
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Divisor.pullbackAlong_liesOver_of_liesOver
    (K F F' E FE F'E : Type*) [Field K] [Field F] [Field F'] [Field E] [Field FE] [Field F'E]
    [Algebra K F] [Algebra K F'] [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE]
      [IsScalarTower K E FE] [IsScalarTower K F FE]
    [Algebra E F'E] [Algebra F' F'E] [Algebra K F'E] [IsScalarTower K E F'E] [IsScalarTower K F'
      F'E]
    [IsAlgClosed K] [CharZero K] [IsAlgClosed E]
    (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')
    (hfgE : ∃ x : FE, Transcendental E x ∧ FiniteDimensional ↥(IntermediateField.adjoin E ({x} :
      Set FE)) FE)
    (hfgE' : ∃ x : F'E, Transcendental E x ∧ FiniteDimensional ↥(IntermediateField.adjoin E ({x} :
      Set F'E)) F'E)
    [AlgebraicCurve.IsCurveOver K F] [AlgebraicCurve.IsCurveOver K F'] [AlgebraicCurve.IsCurveOver
      E FE] [AlgebraicCurve.IsCurveOver E F'E]
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (hgen' : IntermediateField.adjoin E (Set.range (algebraMap F' F'E)) = ⊤)
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (φE : FE →ₐ[E] F'E) (hφE :
      φE.toRingHom.IsIntegral)
    (hcomm : ∀ f : F, φE (algebraMap F FE f) = algebraMap F' F'E (φ f))
    (D : AlgebraicCurve.Divisor K F) (DE : AlgebraicCurve.Divisor E FE)
    (hover : ∀ (v' : AlgebraicCurve.Place E FE) (v : AlgebraicCurve.Place K F),
      v'.toValuationSubring.comap (algebraMap F FE) = v.toValuationSubring → DE v' = D v)
    (hoff : ∀ v' : AlgebraicCurve.Place E FE,
      (∀ v : AlgebraicCurve.Place K F, v'.toValuationSubring.comap (algebraMap F FE) ≠
        v.toValuationSubring) → DE v' = 0) :
    (∀ (w' : AlgebraicCurve.Place E F'E) (w : AlgebraicCurve.Place K F'),
        w'.toValuationSubring.comap (algebraMap F' F'E) = w.toValuationSubring →
        AlgebraicCurve.Divisor.pullbackAlong φE hφE DE w' = AlgebraicCurve.Divisor.pullbackAlong φ
          hφ D w) ∧
    (∀ w' : AlgebraicCurve.Place E F'E,
        (∀ w : AlgebraicCurve.Place K F', w'.toValuationSubring.comap (algebraMap F' F'E) ≠
          w.toValuationSubring) →
        AlgebraicCurve.Divisor.pullbackAlong φE hφE DE w' = 0)

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