Module

HasPrincipalDivisors_of_finiteDimensional_of_isSeparable.lean

Nyll.AlgebraicCurves.Divisors.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable

7 declarations indexed from sourceView source ↗

Module documentation

Algebra, divisors, and base change

Nonzero functions in a finite separable rational-function-field extension have finitely supported order divisors.

Imports7

Nyll.AlgebraicCurves.FunctionFields.CurveOver
Nyll.AlgebraicCurves.Places.Finite_setOf_ord_ne_zero_of_finiteDimensional
Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_hasPrincipalDivisors
Nyll.AlgebraicCurves.Places.Place_sum_ramificationIndex_mul_inertiaDeg_fiberOver
Nyll.AlgebraicCurves.Divisors.Divisor_degree_eq_sum
Mathlib.RingTheory.Norm.Transitivity
Mathlib.FieldTheory.RatFunc.Basic

Imported by2

theorem

degree_eq_finrank_mul

L43 ↗

AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable.HPDfdPort.degree_eq_finrank_mul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable
open AlgebraicCurve Polynomial IntermediateField
noncomputable section
namespace HPDfdPort
section General
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']

Lean source · statement

theorem degree_eq_finrank_mul {g : F}
    {D' : Divisor K F'} (hD' : ∀ w : Place K F', D' w = w.ord (algebraMap F F' g))
    {D : Divisor K F} (hD : ∀ v : Place K F, D v = v.ord g) :
    Divisor.degree D' = (Module.finrank F F' : ℤ) * Divisor.degree D

theorem

ord_prod'

L91 ↗

AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable.HPDfdPort.Place.ord_prod'

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable
open AlgebraicCurve Polynomial IntermediateField
noncomputable section
namespace HPDfdPort
section General
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']

Lean source · statement

theorem Place.ord_prod' {ι : Type*} (v : Place K F') (s : Finset ι)
    (g : ι → F') (hg : ∀ i ∈ s, g i ≠ 0) :
    v.ord (∏ i ∈ s, g i) = ∑ i ∈ s, v.ord (g i)

theorem

sum_smul_apply_eq_ord_prod

L104 ↗

AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable.HPDfdPort.sum_smul_apply_eq_ord_prod

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable
open AlgebraicCurve Polynomial IntermediateField
noncomputable section
namespace HPDfdPort
section General
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
omit [Algebra.IsSeparable F F'] in

Lean source · statement

theorem sum_smul_apply_eq_ord_prod {f : F'} (hf : f ≠ 0)
    {D : Divisor K F'} (hD : ∀ w : Place K F', D w = w.ord f) (w : Place K F') :
    (∑ σ : F' ≃ₐ[F] F', (AlgEquiv.restrictScalars K σ) • D) w
      = w.ord (∏ σ : F' ≃ₐ[F] F', σ f)

theorem

degree_eq_zero_of_isGalois

L117 ↗

AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable.HPDfdPort.degree_eq_zero_of_isGalois

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable
open AlgebraicCurve Polynomial IntermediateField
noncomputable section
namespace HPDfdPort
section General
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']

Lean source · statement

theorem degree_eq_zero_of_isGalois [IsGalois F F'] [HasPrincipalDivisors K F]
    {f : F'} {D : Divisor K F'} (hD : ∀ w : Place K F', D w = w.ord f) :
    Divisor.degree D = 0

theorem

degree_eq_zero_of_tower

L145 ↗

AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable.HPDfdPort.degree_eq_zero_of_tower

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable
open AlgebraicCurve Polynomial IntermediateField
noncomputable section
namespace HPDfdPort
section General
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']

Lean source · statement

theorem degree_eq_zero_of_tower
    (htop : ∀ (h : F') (E : Divisor K F'), (∀ w : Place K F', E w = w.ord h) →
      Divisor.degree E = 0)
    (hex : ∀ h : F', h ≠ 0 → ∃ E : Divisor K F', ∀ w : Place K F', E w = w.ord h)
    {f : F} {D : Divisor K F} (hD : ∀ v : Place K F, D v = v.ord f) :
    Divisor.degree D = 0

def

principalDivisorOf

L170 ↗

AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable.HPDfdPort.principalDivisorOf

Documentation

The finitely supported divisor whose coefficients are the orders of the given nonzero function.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable
open AlgebraicCurve Polynomial IntermediateField
noncomputable section
namespace HPDfdPort
variable {K : Type*} [Field K] {F' : Type*} [Field F'] [Algebra K F']
  [Algebra (RatFunc K) F'] [IsScalarTower K (RatFunc K) F']
  [FiniteDimensional (RatFunc K) F'] [Algebra.IsSeparable (RatFunc K) F']

Lean source · statement

def principalDivisorOf {f : F'} (hf : f ≠ 0) : AlgebraicCurve.Divisor K F'

theorem