Module

Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.lean

Nyll.AlgebraicCurves.Divisors.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq

45 declarations indexed from sourceView source ↗

Module documentation

Divisor exists Unique pullback Constants eq of forall smul eq

Imports6

Imported by1

Nyll.AlgebraicCurves.Divisors.All

theorem

inv_notMem_of_mem_nonunits

L39 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.inv_notMem_of_mem_nonunits

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem inv_notMem_of_mem_nonunits (B : ValuationSubring L) {x : L} (hx0 : x ≠ 0)
    (hx : x ∈ B.nonunits) : x⁻¹ ∉ B

theorem

mem_nonunits_of_inv_notMem

L47 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.mem_nonunits_of_inv_notMem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem mem_nonunits_of_inv_notMem (B : ValuationSubring L) {x : L} (hx : x⁻¹ ∉ B) :
    x ∈ B.nonunits

theorem

mem_nonunits_iff_inv_notMem

L58 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.mem_nonunits_iff_inv_notMem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem mem_nonunits_iff_inv_notMem (B : ValuationSubring L) {x : L} (hx0 : x ≠ 0) :
    x ∈ B.nonunits ↔ x⁻¹ ∉ B

theorem

zero_mem_nonunits

L62 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.zero_mem_nonunits

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem zero_mem_nonunits (B : ValuationSubring L) : (0 : L) ∈ B.nonunits

theorem

sub_mem_nonunits

L66 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.sub_mem_nonunits

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem sub_mem_nonunits (B : ValuationSubring L) {x y : L} (hx : x ∈ B.nonunits)
    (hy : y ∈ B.nonunits) : x - y ∈ B.nonunits

theorem

add_mem_nonunits

L71 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.add_mem_nonunits

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem add_mem_nonunits (B : ValuationSubring L) {x y : L} (hx : x ∈ B.nonunits)
    (hy : y ∈ B.nonunits) : x + y ∈ B.nonunits

theorem

nonunits_le

L76 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.nonunits_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem nonunits_le (B : ValuationSubring L) {x : L} (hx : x ∈ B.nonunits) : x ∈ B

theorem

mk_mem_maximalIdeal_iff_mem_nonunits

L79 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.mk_mem_maximalIdeal_iff_mem_nonunits

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem mk_mem_maximalIdeal_iff_mem_nonunits (B : ValuationSubring L) {x : L} (hx : x ∈ B) :
    (⟨x, hx⟩ : B) ∈ maximalIdeal B ↔ x ∈ B.nonunits

theorem

mem_nonunits_iff_of_forall_mem_iff

L84 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.mem_nonunits_iff_of_forall_mem_iff

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem mem_nonunits_iff_of_forall_mem_iff {L' : Type*} [Field L'] {E : Type*} [FunLike E L L']
    [RingHomClass E L L'] (g : E) (A : ValuationSubring L) (B : ValuationSubring L')
    (h : ∀ x, x ∈ A ↔ g x ∈ B) (x : L) : x ∈ A.nonunits ↔ g x ∈ B.nonunits

theorem

eq_zero_of_algebraMap_mem_nonunits

L98 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.eq_zero_of_algebraMap_mem_nonunits

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem eq_zero_of_algebraMap_mem_nonunits (W : Place K F) {a : K}
    (ha : algebraMap K F a ∈ W.toValuationSubring.nonunits) : a = 0

def

ResBij

L107 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.ResBij

Documentation

The condition that the base field maps bijectively onto the residue field of the place.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def ResBij (W : Place K F) : Prop

theorem

resBij_of_isAlgClosed

L109 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.resBij_of_isAlgClosed

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resBij_of_isAlgClosed [IsAlgClosed K] [IsCurveOver K F] (W : Place K F) : ResBij W

def

resHom

L115 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.resHom

Documentation

The residue map to K obtained from the bijectivity of the map to the residue field.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def resHom (W : Place K F) (hW : ResBij W) : W.toValuationSubring →ₐ[K] K

theorem

resHom_apply

L126 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.resHom_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resHom_apply (W : Place K F) (hW : ResBij W) (g : W.toValuationSubring) :
    resHom W hW g = (RingEquiv.ofBijective (algebraMap K W.ResidueField) hW).symm
      (IsLocalRing.residue _ g)

theorem

algebraMap_resHom

L130 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.algebraMap_resHom

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem algebraMap_resHom (W : Place K F) (hW : ResBij W) (g : W.toValuationSubring) :
    algebraMap K W.ResidueField (resHom W hW g) = IsLocalRing.residue _ g

theorem

resHom_spec

L135 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.resHom_spec

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resHom_spec (W : Place K F) (hW : ResBij W) (g : W.toValuationSubring) :
    (g : F) - algebraMap K F (resHom W hW g) ∈ W.toValuationSubring.nonunits

theorem

resHom_eq_iff

L146 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.resHom_eq_iff

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resHom_eq_iff (W : Place K F) (hW : ResBij W) (g : W.toValuationSubring) (a : K) :
    resHom W hW g = a ↔ (g : F) - algebraMap K F a ∈ W.toValuationSubring.nonunits

theorem

mem_nonunits_iff_resHom_eq_zero

L161 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.mem_nonunits_iff_resHom_eq_zero

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_nonunits_iff_resHom_eq_zero (W : Place K F) (hW : ResBij W)
    (g : W.toValuationSubring) :
    (g : F) ∈ W.toValuationSubring.nonunits ↔ resHom W hW g = 0

theorem

resHom_eq_of_sub_mem_nonunits

L166 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.resHom_eq_of_sub_mem_nonunits

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resHom_eq_of_sub_mem_nonunits (W : Place K F) (hW : ResBij W)
    (g g' : W.toValuationSubring) (h : (g : F) - g' ∈ W.toValuationSubring.nonunits) :
    resHom W hW g = resHom W hW g'

theorem

coe_aeval_mk

L175 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.coe_aeval_mk

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem coe_aeval_mk (W : Place K F) {x : F} (hx : x ∈ W.toValuationSubring) (P : K[X]) :
    ((aeval (⟨x, hx⟩ : W.toValuationSubring) P : W.toValuationSubring) : F) = aeval x P

theorem

aeval_mem

L180 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.aeval_mem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem aeval_mem (W : Place K F) {x : F} (hx : x ∈ W.toValuationSubring) (P : K[X]) :
    aeval x P ∈ W.toValuationSubring

theorem

resHom_aeval

L185 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.resHom_aeval

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resHom_aeval (W : Place K F) (hW : ResBij W) {x : F} (hx : x ∈ W.toValuationSubring)
    (P : K[X]) :
    resHom W hW ⟨aeval x P, aeval_mem W hx P⟩ = P.eval (resHom W hW ⟨x, hx⟩)

def

Over

L205 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.Over

Documentation

The condition that the extended place restricts to the given place of the original function field.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Over
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

def Over (v : Place k F₀) (W : Place K F) : Prop

theorem

mem_iff_of_over

L208 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.mem_iff_of_over

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Over
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem mem_iff_of_over {v : Place k F₀} {W : Place K F} (hW : Over v W) (f : F₀) :
    f ∈ v.toValuationSubring ↔ ι f ∈ W.toValuationSubring

theorem

nonunits_iff_of_over

L213 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.nonunits_iff_of_over

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Over
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem nonunits_iff_of_over {v : Place k F₀} {W : Place K F} (hW : Over v W) (f : F₀) :
    ι f ∈ W.toValuationSubring.nonunits ↔ f ∈ v.toValuationSubring.nonunits

theorem

mem_smul_place_iff

L224 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.mem_smul_place_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Over
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
local notation "ι" => algebraMap F₀ F
open scoped Pointwise

Lean source · statement

theorem mem_smul_place_iff (g : SemilinearAut K F) (W : Place K F) (x : F) :
    x ∈ (g • W).toValuationSubring ↔ g⁻¹ • x ∈ W.toValuationSubring

theorem

smul_mem_smul_place_iff

L229 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.smul_mem_smul_place_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Over
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
local notation "ι" => algebraMap F₀ F
open scoped Pointwise

Lean source · statement

theorem smul_mem_smul_place_iff (g : SemilinearAut K F) (W : Place K F) (x : F) :
    g • x ∈ (g • W).toValuationSubring ↔ x ∈ W.toValuationSubring

theorem

smul_mem_nonunits_smul_iff

L234 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.smul_mem_nonunits_smul_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Over
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
local notation "ι" => algebraMap F₀ F
open scoped Pointwise

Lean source · statement

theorem smul_mem_nonunits_smul_iff (g : SemilinearAut K F) (W : Place K F) (x : F) :
    g • x ∈ (g • W).toValuationSubring.nonunits ↔ x ∈ W.toValuationSubring.nonunits

theorem

over_smul

L240 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.over_smul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Over
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
local notation "ι" => algebraMap F₀ F
open scoped Pointwise

Lean source · statement

theorem over_smul {v : Place k F₀} {W : Place K F} (hW : Over v W) (g : SemilinearAut K F)
    (hg : ∀ x : F₀, g • ι x = ι x) : Over v (g • W)

theorem

theta_mem

L262 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.theta_mem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Transitive
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem theta_mem {v : Place k F₀} {W : Place K F} (hW : Over v W) (θ : v.toValuationSubring) :
    ι (θ : F₀) ∈ W.toValuationSubring

def

αv

L267 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.αv

Documentation

The base-field residue of an integral element at a place above the original place.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Transitive
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

def αv {v : Place k F₀} (W : Place K F) (hb : ResBij W) (hW : Over v W)
    (θ : v.toValuationSubring) : K

theorem

theta_sub_alpha_mem

L271 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.theta_sub_alpha_mem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Transitive
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem theta_sub_alpha_mem {v : Place k F₀} {W : Place K F} (hb : ResBij W) (hW : Over v W)
    (θ : v.toValuationSubring) :
    ι (θ : F₀) - algebraMap K F (αv W hb hW θ) ∈ W.toValuationSubring.nonunits

theorem

alpha_eq_of_mem_nonunits

L276 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.alpha_eq_of_mem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Transitive
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem alpha_eq_of_mem_nonunits {v : Place k F₀} {W : Place K F} (hb : ResBij W) (hW : Over v W)
    (θ : v.toValuationSubring) {a : K}
    (h : ι (θ : F₀) - algebraMap K F a ∈ W.toValuationSubring.nonunits) : αv W hb hW θ = a

theorem

coe_aeval

L281 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.coe_aeval

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Transitive
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem coe_aeval (v : Place k F₀) (θ : v.toValuationSubring) (P : k[X]) :
    ((aeval θ P : v.toValuationSubring) : F₀) = aeval (θ : F₀) P

theorem

algebraMap_aeval

L285 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.algebraMap_aeval

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Transitive
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem algebraMap_aeval (θ : F₀) (P : k[X]) :
    ι (aeval θ P) = aeval (ι θ) (P.map (algebraMap k K))

theorem

resHom_algebraMap_aeval

L289 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.resHom_algebraMap_aeval

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Transitive
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · full declaration

theorem resHom_algebraMap_aeval {v : Place k F₀} {W : Place K F} (hb : ResBij W) (hW : Over v W)
    (θ : v.toValuationSubring) (P : k[X]) :
    resHom W hb ⟨ι (aeval (θ : F₀) P), (mem_iff_of_over hW _).mp (by
        rw [← coe_aeval]; exact Subtype.mem _)⟩
      = (P.map (algebraMap k K)).eval (αv W hb hW θ) := by
  have hΘ := theta_mem hW θ
  have h1 : (⟨ι (aeval (θ : F₀) P), (mem_iff_of_over hW _).mp (by
        rw [← coe_aeval]; exact Subtype.mem _)⟩ : W.toValuationSubring)
      = ⟨aeval (ι (θ : F₀)) (P.map (algebraMap k K)), aeval_mem W hΘ _⟩ := by
    apply Subtype.ext
    exact algebraMap_aeval (θ : F₀) P
  rw [h1, resHom_aeval]
  rfl

theorem

isRoot_alpha

L303 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.isRoot_alpha

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Transitive
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem isRoot_alpha {v : Place k F₀} {W : Place K F} (hb : ResBij W) (hW : Over v W)
    (θ : v.toValuationSubring) :
    ((minpoly k (IsLocalRing.residue _ θ)).map (algebraMap k K)).IsRoot (αv W hb hW θ)

def

α

L329 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.α

Documentation

The residue value in the algebraically closed constant field at the extending place.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Transitive
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
variable [IsAlgClosed K] [IsCurveOver K F]

Lean source · statement

def α {v : Place k F₀} (θ : v.toValuationSubring) (W : Place K F) (hW : Over v W) : K

theorem

alpha_smul

L332 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.alpha_smul

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Transitive
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
variable [IsAlgClosed K] [IsCurveOver K F]
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem alpha_smul {v : Place k F₀} (θ : v.toValuationSubring) {W : Place K F} (hW : Over v W)
    (g : SemilinearAut K F) (hg : ∀ x : F₀, g • ι x = ι x) :
    α θ (g • W) (over_smul hW g hg) = SemilinearAut.baseAut g (α θ W hW)

theorem

eq_of_alpha_eq

L341 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.eq_of_alpha_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Transitive
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
variable [IsAlgClosed K] [IsCurveOver K F]

Lean source · statement

theorem eq_of_alpha_eq [PerfectField k] [IsCurveOver k F₀]
    (hfg : ∃ s : Finset F₀, IntermediateField.adjoin k (s : Set F₀) = ⊤)
    (hgen : IntermediateField.adjoin K (Set.range (algebraMap F₀ F)) = ⊤)
    (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)
    {v : Place k F₀} (θ : v.toValuationSubring)
    (hθ : IntermediateField.adjoin k {IsLocalRing.residue _ θ} = ⊤)
    {W₁ W₂ : Place K F} (h₁ : Over v W₁) (h₂ : Over v W₂)
    (hα : α θ W₁ h₁ = α θ W₂ h₂) : W₁ = W₂

theorem

exists_smul_eq_of_over

L392 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.exists_smul_eq_of_over

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Transitive
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
variable [IsAlgClosed K] [IsCurveOver K F]

Lean source · statement

theorem exists_smul_eq_of_over [PerfectField k] [IsCurveOver k F₀]
    (hfg : ∃ s : Finset F₀, IntermediateField.adjoin k (s : Set F₀) = ⊤)
    (hgen : IntermediateField.adjoin K (Set.range (algebraMap F₀ F)) = ⊤)
    (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)
    (G : Subgroup (SemilinearAut K F))
    (hG₀ : ∀ g ∈ G, ∀ x : F₀, g • ι x = ι x)
    (hGK : ∀ a : K, (∀ g ∈ G, SemilinearAut.baseAut g a = a) → a ∈ Set.range (algebraMap k K))
    {v : Place k F₀} {W₁ W₂ : Place K F} (h₁ : Over v W₁) (h₂ : Over v W₂) :
    ∃ g ∈ G, g • W₁ = W₂

theorem

hconst_of_hLD

L493 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.hconst_of_hLD

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Hyps
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]

Lean source · statement

theorem hconst_of_hLD [IsAlgClosed K]
    (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0) :
    ∀ y : F₀, IsAlgebraic k y → y ∈ (algebraMap k F₀).range

theorem

adjoin_range_eq_top

L522 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.adjoin_range_eq_top

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Hyps
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]

Lean source · statement

theorem adjoin_range_eq_top [Algebra.IsIntegral F₀ F]
    (hgen : IntermediateField.adjoin K (Set.range (algebraMap F₀ F)) = ⊤) :
    Algebra.adjoin F₀ (Set.range (algebraMap K F)) = ⊤

theorem

main

L564 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq.P2mSchmidtDescent2.main

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
noncomputable section
open Polynomial IsLocalRing AlgebraicCurve
namespace P2mSchmidtDescent2
section Descent
variable {k K F₀ F : Type*} [Field k] [PerfectField k] [Field K] [IsAlgClosed K]
  [Field F₀] [Field F] [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
  [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
  [Algebra.IsAlgebraic k K] [Algebra.IsIntegral F₀ F]
  [IsCurveOver k F₀] [IsCurveOver K F]

Lean source · statement

theorem main
    (hfg : ∃ s : Finset F₀, IntermediateField.adjoin k (s : Set F₀) = ⊤)
    (hgen : IntermediateField.adjoin K (Set.range (algebraMap F₀ F)) = ⊤)
    (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)
    (G : Subgroup (SemilinearAut K F))
    (hG₀ : ∀ g ∈ G, ∀ x : F₀, g • algebraMap F₀ F x = algebraMap F₀ F x)
    (hGK : ∀ a : K, (∀ g ∈ G, SemilinearAut.baseAut g a = a) → a ∈ Set.range (algebraMap k K))
    (D : Divisor K F) (hD : ∀ g ∈ G, g • D = D) :
    ∃! D₀ : Divisor k F₀, Divisor.pullbackConstants K F D₀ = D

theorem

existsUnique_pullbackConstants_eq_of_forall_smul_eq

L623 ↗

AlgebraicCurve.Divisor.existsUnique_pullbackConstants_eq_of_forall_smul_eq

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
open P2mSchmidtDescent2 in

Lean source · statement

theorem _root_.AlgebraicCurve.Divisor.existsUnique_pullbackConstants_eq_of_forall_smul_eq
    {k K F₀ F : Type*} [Field k] [PerfectField k] [Field K] [IsAlgClosed K]
    [Field F₀] [Field F] [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
    [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
    [Algebra.IsAlgebraic k K] [Algebra.IsIntegral F₀ F]
    [AlgebraicCurve.IsCurveOver k F₀] [AlgebraicCurve.IsCurveOver K F]
    (hfg : ∃ s : Finset F₀, IntermediateField.adjoin k (s : Set F₀) = ⊤)
    (hgen : IntermediateField.adjoin K (Set.range (algebraMap F₀ F)) = ⊤)
    (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)
    (G : Subgroup (AlgebraicCurve.SemilinearAut K F))
    (hG₀ : ∀ g ∈ G, ∀ x : F₀, g • algebraMap F₀ F x = algebraMap F₀ F x)
    (hGK : ∀ a : K, (∀ g ∈ G, AlgebraicCurve.SemilinearAut.baseAut g a = a) →
      a ∈ Set.range (algebraMap k K))
    (D : AlgebraicCurve.Divisor K F) (hD : ∀ g ∈ G, g • D = D) :
    ∃! D₀ : AlgebraicCurve.Divisor k F₀,
      AlgebraicCurve.Divisor.pullbackConstants K F D₀ = D

Module documentation

Divisor exists Unique pullback Constants eq of forall smul eq

Declarations