NYLL
Module

Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension.lean

Nyll.AlgebraicCurves.Divisors.Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension
7 declarations indexed from sourceView source ↗

Module documentation

Divisor is Principal of is Principal pullback Constants of is Constant Field Extension

Imports3
Imported by1

Declarations

theorem

ord_nonneg_of_mem

L44 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension.P2mConormPrincipalDescent.ord_nonneg_of_mem
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
namespace P2mConormPrincipalDescent
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem ord_nonneg_of_mem {f : L} (hf : f ∈ w.toValuationSubring) : 0 ≤ w.ord f
theorem

ord_algebraMap

L49 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension.P2mConormPrincipalDescent.ord_algebraMap
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
namespace P2mConormPrincipalDescent
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem ord_algebraMap (a : k) : w.ord (algebraMap k L a) = 0
theorem

mem_range_of_isAlgebraic

L57 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension.P2mConormPrincipalDescent.mem_range_of_isAlgebraic
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
namespace P2mConormPrincipalDescent
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem mem_range_of_isAlgebraic (hC : ConstantsAreBase k L) (y : L) (hy : IsAlgebraic k y) :
    y ∈ (algebraMap k L).range
theorem

ord_eq_zero_of_mem_lSpace_zero

L71 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension.P2mConormPrincipalDescent.ord_eq_zero_of_mem_lSpace_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
namespace P2mConormPrincipalDescent
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem ord_eq_zero_of_mem_lSpace_zero (hC : ConstantsAreBase k L) {f : L}
    (hf : f ∈ LSpace (0 : Divisor k L)) (v : Place k L) : v.ord f = 0
theorem

exists_ne_zero_mem_lSpace

L88 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension.P2mConormPrincipalDescent.exists_ne_zero_mem_lSpace
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
namespace P2mConormPrincipalDescent
section Main
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
    [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
    [HasPrincipalDivisors K' F']
Lean source · statement
theorem exists_ne_zero_mem_lSpace
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (E : Divisor K F) (hE : (Divisor.pullbackConstants K' F' E).IsPrincipal) :
    ∃ x : F, x ≠ 0 ∧ x ∈ LSpace E
theorem

isPrincipal_of_isPrincipal_pullbackConstants

L113 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension.P2mConormPrincipalDescent.isPrincipal_of_isPrincipal_pullbackConstants
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
namespace P2mConormPrincipalDescent
section Main
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
    [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
    [HasPrincipalDivisors K' F']
Lean source · statement
theorem isPrincipal_of_isPrincipal_pullbackConstants
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hC : ConstantsAreBase K F)
    {D : Divisor K F} (hD : (Divisor.pullbackConstants K' F' D).IsPrincipal) :
    D.IsPrincipal
theorem

isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension

L157 ↗
AlgebraicCurve.Divisor.isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurve.Divisor
open _root_.AlgebraicCurves.Divisors.Proofs in
open Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension in
open AlgebraicCurve in
open P2mConormPrincipalDescent in
Lean source · statement
theorem isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension
    {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
    [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
    [AlgebraicCurve.HasPrincipalDivisors K' F']
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hC : AlgebraicCurve.ConstantsAreBase K F)
    {D : AlgebraicCurve.Divisor K F}
    (hD : (AlgebraicCurve.Divisor.pullbackConstants K' F' D).IsPrincipal) :
    D.IsPrincipal

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