NYLL
Module

Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.lean

Nyll.AlgebraicCurves.Divisors.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
21 declarations indexed from sourceView source ↗

Module documentation

Divisor map Domain pullback Along eq and restrict Along eq of deg Zero

Imports1
Imported by1

Declarations

theorem

mapDomain_apply_eq_sum

L36 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.mapDomain_apply_eq_sum
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Finsupp
variable {X Y : Type*}
Lean source · full declaration
theorem mapDomain_apply_eq_sum [DecidableEq Y] (r : X → Y) (D : X →₀ ℤ) (y : Y) :
    mapDomain r D y = ∑ x ∈ D.support, if r x = y then D x else 0 := by
  simp only [Finsupp.mapDomain, Finsupp.sum, Finsupp.finsetSum_apply, Finsupp.single_apply]
theorem

mapDomain_nonneg

L40 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.mapDomain_nonneg
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Finsupp
variable {X Y : Type*}
Lean source · statement
theorem mapDomain_nonneg (r : X → Y) {D : X →₀ ℤ} (hD : ∀ x, 0 ≤ D x) (y : Y) :
    0 ≤ mapDomain r D y
theorem

le_mapDomain_apply_self

L49 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.le_mapDomain_apply_self
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Finsupp
variable {X Y : Type*}
Lean source · statement
theorem le_mapDomain_apply_self (r : X → Y) {D : X →₀ ℤ} (hD : ∀ x, 0 ≤ D x) (x : X) :
    D x ≤ mapDomain r D (r x)
theorem

degree_eq_sum

L69 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.degree_eq_sum
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Rational
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem degree_eq_sum (h1 : ∀ v : Place K F, v.deg = 1) (D : Divisor K F) :
    Divisor.degree D = ∑ v ∈ D.support, D v
theorem

degree_nonneg

L75 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.degree_nonneg
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Rational
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem degree_nonneg (h1 : ∀ v : Place K F, v.deg = 1) {D : Divisor K F}
    (hD : ∀ v, 0 ≤ D v) : 0 ≤ Divisor.degree D
theorem

eq_zero_of_nonneg_of_degree_eq_zero

L80 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.eq_zero_of_nonneg_of_degree_eq_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Rational
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem eq_zero_of_nonneg_of_degree_eq_zero (h1 : ∀ v : Place K F, v.deg = 1)
    {D : Divisor K F} (hD : ∀ v, 0 ≤ D v) (hdeg : Divisor.degree D = 0) : D = 0
theorem

degree_mapDomain_eq

L89 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.degree_mapDomain_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Rational
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem degree_mapDomain_eq {K' F' : Type*} [Field K'] [Field F'] [Algebra K' F']
    (h1 : ∀ v : Place K F, v.deg = 1) (h1' : ∀ w : Place K' F', w.deg = 1)
    (r : Place K F → Place K' F') (D : Divisor K F) :
    Divisor.degree (mapDomain r D) = Divisor.degree D
theorem

ramificationIndexAlong_pos

L108 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.ramificationIndexAlong_pos
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Along
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
omit [HasPrincipalDivisors K F'] in
include hφ in
Lean source · statement
theorem ramificationIndexAlong_pos (w : Place K F') : 0 < Place.ramificationIndexAlong φ w
theorem

pullbackAlong_nonneg

L114 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.pullbackAlong_nonneg
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Along
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
Lean source · statement
theorem pullbackAlong_nonneg {D : Divisor K F} (hD : ∀ v, 0 ≤ D v) (w : Place K F') :
    0 ≤ Divisor.pullbackAlong φ hφ D w
theorem

single_one_nonneg

L119 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.single_one_nonneg
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Along
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
Lean source · statement
theorem single_one_nonneg {X : Type*} (x : X) : ∀ x', 0 ≤ (single x (1 : ℤ)) x'
theorem

pullbackAlong_single_nonneg

L125 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.pullbackAlong_single_nonneg
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Along
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
Lean source · statement
theorem pullbackAlong_single_nonneg (v : Place K F) (w : Place K F') :
    0 ≤ Divisor.pullbackAlong φ hφ (single v 1) w
theorem

pullbackAlong_single_apply_of_ne

L129 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.pullbackAlong_single_apply_of_ne
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Along
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
Lean source · statement
theorem pullbackAlong_single_apply_of_ne {v : Place K F} {w : Place K F'}
    (h : w.restrictAlong φ hφ ≠ v) : Divisor.pullbackAlong φ hφ (single v 1) w = 0
theorem

pullbackAlong_single_apply_self

L134 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.pullbackAlong_single_apply_self
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Along
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
Lean source · statement
theorem pullbackAlong_single_apply_self (w : Place K F') :
    Divisor.pullbackAlong φ hφ (single (w.restrictAlong φ hφ) 1) w
      = Place.ramificationIndexAlong φ w
theorem

inertiaDegAlong_eq_one

L139 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.inertiaDegAlong_eq_one
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Along
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
omit [HasPrincipalDivisors K F'] in
Lean source · statement
theorem inertiaDegAlong_eq_one (h1F : ∀ v : Place K F, v.deg = 1)
    (h1F' : ∀ w : Place K F', w.deg = 1) (w : Place K F') :
    (w.inertiaDegAlong φ hφ : ℤ) = 1
theorem

pushforwardAlong_single_one

L148 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.pushforwardAlong_single_one
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Along
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
omit [HasPrincipalDivisors K F'] in
Lean source · statement
theorem pushforwardAlong_single_one (h1F : ∀ v : Place K F, v.deg = 1)
    (h1F' : ∀ w : Place K F', w.deg = 1) (w : Place K F') :
    Divisor.pushforwardAlong φ hφ (single w 1) = single (w.restrictAlong φ hφ) 1
def

defect

L165 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.defect
Documentation

The difference between reducing a pulled-back place divisor and pulling back its reduction.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Engine
variable {K F₁ F₂ : Type*} [Field K] [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable {k C₁ C₂ : Type*} [Field k] [Field C₁] [Field C₂] [Algebra k C₁] [Algebra k C₂]
variable [HasPrincipalDivisors K F₂] [HasPrincipalDivisors k C₂]
variable (φ : F₁ →ₐ[K] F₂) (hφ : φ.toRingHom.IsIntegral)
variable (φb : C₁ →ₐ[k] C₂) (hφb : φb.toRingHom.IsIntegral)
variable (r₁ : Place K F₁ → Place k C₁) (r : Place K F₂ → Place k C₂)
Lean source · statement
def defect (v : Place K F₁) : Divisor k C₂
theorem

defect_eq

L169 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.defect_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Engine
variable {K F₁ F₂ : Type*} [Field K] [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable {k C₁ C₂ : Type*} [Field k] [Field C₁] [Field C₂] [Algebra k C₁] [Algebra k C₂]
variable [HasPrincipalDivisors K F₂] [HasPrincipalDivisors k C₂]
variable (φ : F₁ →ₐ[K] F₂) (hφ : φ.toRingHom.IsIntegral)
variable (φb : C₁ →ₐ[k] C₂) (hφb : φb.toRingHom.IsIntegral)
variable (r₁ : Place K F₁ → Place k C₁) (r : Place K F₂ → Place k C₂)
Lean source · statement
theorem defect_eq
    (h1F₁ : ∀ v : Place K F₁, v.deg = 1)
    (hcompat : ∀ D : Divisor K F₁, D ∈ Divisor.degZero (K := K) (F := F₁) →
      mapDomain r (Divisor.pullbackAlong φ hφ D) =
        Divisor.pullbackAlong φb hφb (mapDomain r₁ D))
    (v v' : Place K F₁) :
    defect φ hφ φb hφb r₁ r v = defect φ hφ φb hφb r₁ r v'
theorem

defect_nonneg

L184 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.defect_nonneg
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Engine
variable {K F₁ F₂ : Type*} [Field K] [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable {k C₁ C₂ : Type*} [Field k] [Field C₁] [Field C₂] [Algebra k C₁] [Algebra k C₂]
variable [HasPrincipalDivisors K F₂] [HasPrincipalDivisors k C₂]
variable (φ : F₁ →ₐ[K] F₂) (hφ : φ.toRingHom.IsIntegral)
variable (φb : C₁ →ₐ[k] C₂) (hφb : φb.toRingHom.IsIntegral)
variable (r₁ : Place K F₁ → Place k C₁) (r : Place K F₂ → Place k C₂)
Lean source · statement
theorem defect_nonneg
    (h1F₁ : ∀ v : Place K F₁, v.deg = 1)
    (hcompat : ∀ D : Divisor K F₁, D ∈ Divisor.degZero (K := K) (F := F₁) →
      mapDomain r (Divisor.pullbackAlong φ hφ D) =
        Divisor.pullbackAlong φb hφb (mapDomain r₁ D))
    (hnc : ∀ v : Place K F₁, ∃ v' : Place K F₁, r₁ v' ≠ r₁ v)
    (v : Place K F₁) (Y : Place k C₂) : 0 ≤ defect φ hφ φb hφb r₁ r v Y
theorem

defect_eq_zero

L200 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.defect_eq_zero
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Engine
variable {K F₁ F₂ : Type*} [Field K] [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable {k C₁ C₂ : Type*} [Field k] [Field C₁] [Field C₂] [Algebra k C₁] [Algebra k C₂]
variable [HasPrincipalDivisors K F₂] [HasPrincipalDivisors k C₂]
variable (φ : F₁ →ₐ[K] F₂) (hφ : φ.toRingHom.IsIntegral)
variable (φb : C₁ →ₐ[k] C₂) (hφb : φb.toRingHom.IsIntegral)
variable (r₁ : Place K F₁ → Place k C₁) (r : Place K F₂ → Place k C₂)
Lean source · statement
theorem defect_eq_zero
    (h1F₁ : ∀ v : Place K F₁, v.deg = 1) (h1F₂ : ∀ W : Place K F₂, W.deg = 1)
    (h1C₂ : ∀ Y : Place k C₂, Y.deg = 1)
    (hcompat : ∀ D : Divisor K F₁, D ∈ Divisor.degZero (K := K) (F := F₁) →
      mapDomain r (Divisor.pullbackAlong φ hφ D) =
        Divisor.pullbackAlong φb hφb (mapDomain r₁ D))
    (hdeg : ∀ v : Place K F₁,
      Divisor.degree (Divisor.pullbackAlong φ hφ (single v 1)) ≤
        Divisor.degree (Divisor.pullbackAlong φb hφb (single (r₁ v) 1)))
    (hnc : ∀ v : Place K F₁, ∃ v' : Place K F₁, r₁ v' ≠ r₁ v)
    (v : Place K F₁) : defect φ hφ φb hφb r₁ r v = 0
theorem

engine

L219 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero.P2mSolDeuringCriterion.engine
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
noncomputable section
namespace P2mSolDeuringCriterion
open Finsupp
section Engine
variable {K F₁ F₂ : Type*} [Field K] [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable {k C₁ C₂ : Type*} [Field k] [Field C₁] [Field C₂] [Algebra k C₁] [Algebra k C₂]
variable [HasPrincipalDivisors K F₂] [HasPrincipalDivisors k C₂]
variable (φ : F₁ →ₐ[K] F₂) (hφ : φ.toRingHom.IsIntegral)
variable (φb : C₁ →ₐ[k] C₂) (hφb : φb.toRingHom.IsIntegral)
variable (r₁ : Place K F₁ → Place k C₁) (r : Place K F₂ → Place k C₂)
Lean source · statement
theorem engine
    (h1F₁ : ∀ v : Place K F₁, v.deg = 1) (h1F₂ : ∀ W : Place K F₂, W.deg = 1)
    (h1C₁ : ∀ Q : Place k C₁, Q.deg = 1) (h1C₂ : ∀ Y : Place k C₂, Y.deg = 1)
    (hcompat : ∀ D : Divisor K F₁, D ∈ Divisor.degZero (K := K) (F := F₁) →
      mapDomain r (Divisor.pullbackAlong φ hφ D) =
        Divisor.pullbackAlong φb hφb (mapDomain r₁ D))
    (hdeg : ∀ v : Place K F₁,
      Divisor.degree (Divisor.pullbackAlong φ hφ (single v 1)) ≤
        Divisor.degree (Divisor.pullbackAlong φb hφb (single (r₁ v) 1)))
    (hnc : ∀ v : Place K F₁, ∃ v' : Place K F₁, r₁ v' ≠ r₁ v) :
    (∀ D : Divisor K F₁, mapDomain r (Divisor.pullbackAlong φ hφ D) =
        Divisor.pullbackAlong φb hφb (mapDomain r₁ D)) ∧
    (∀ W : Place K F₂, (r W).restrictAlong φb hφb = r₁ (W.restrictAlong φ hφ)) ∧
    (∀ D : Divisor K F₂, mapDomain r₁ (Divisor.pushforwardAlong φ hφ D) =
        Divisor.pushforwardAlong φb hφb (mapDomain r D))
theorem

mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero

L278 ↗
AlgebraicCurve.Divisor.mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
open AlgebraicCurve
open P2mSolDeuringCriterion in
Lean source · statement
theorem _root_.AlgebraicCurve.Divisor.mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
    {K F₁ F₂ : Type*} [Field K] [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
    {k C₁ C₂ : Type*} [Field k] [Field C₁] [Field C₂] [Algebra k C₁] [Algebra k C₂]
    [HasPrincipalDivisors K F₂] [HasPrincipalDivisors k C₂]
    (φ : F₁ →ₐ[K] F₂) (hφ : φ.toRingHom.IsIntegral)
    (φb : C₁ →ₐ[k] C₂) (hφb : φb.toRingHom.IsIntegral)
    (r₁ : Place K F₁ → Place k C₁) (r : Place K F₂ → Place k C₂)
    (h1F₁ : ∀ v : Place K F₁, v.deg = 1) (h1F₂ : ∀ W : Place K F₂, W.deg = 1)
    (h1C₁ : ∀ Q : Place k C₁, Q.deg = 1) (h1C₂ : ∀ Y : Place k C₂, Y.deg = 1)
    (hcompat : ∀ D : Divisor K F₁, D ∈ Divisor.degZero (K := K) (F := F₁) →
      Finsupp.mapDomain r (Divisor.pullbackAlong φ hφ D) =
        Divisor.pullbackAlong φb hφb (Finsupp.mapDomain r₁ D))
    (hdeg : ∀ v : Place K F₁,
      Divisor.degree (Divisor.pullbackAlong φ hφ (Finsupp.single v 1)) ≤
        Divisor.degree (Divisor.pullbackAlong φb hφb (Finsupp.single (r₁ v) 1)))
    (hnc : ∀ v : Place K F₁, ∃ v' : Place K F₁, r₁ v' ≠ r₁ v) :
    (∀ D : Divisor K F₁, Finsupp.mapDomain r (Divisor.pullbackAlong φ hφ D) =
        Divisor.pullbackAlong φb hφb (Finsupp.mapDomain r₁ D)) ∧
    (∀ W : Place K F₂, (r W).restrictAlong φb hφb = r₁ (W.restrictAlong φ hφ)) ∧
    (∀ D : Divisor K F₂, Finsupp.mapDomain r₁ (Divisor.pushforwardAlong φ hφ D) =
        Divisor.pushforwardAlong φb hφb (Finsupp.mapDomain r D))

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