Module

Divisor_pushforwardAlong_comp.lean

Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardAlong_comp

4 declarations indexed from sourceView source ↗

Module documentation

Divisor pushforward Along comp

Imports1

Nyll.AlgebraicCurves.Divisors.Correspondences

Imported by2

def

valuationSubringEquivOfEq

L26 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_comp.valuationSubringEquivOfEq

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_comp
open AlgebraicCurve

Lean source · statement

def valuationSubringEquivOfEq
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v v' : Place K F) (h : v = v') : v.toValuationSubring ≃+* v'.toValuationSubring

theorem

coe_valuationSubringEquivOfEq

L32 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_comp.coe_valuationSubringEquivOfEq

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_comp
open AlgebraicCurve

Lean source · statement

theorem coe_valuationSubringEquivOfEq
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v v' : Place K F) (h : v = v') (a : v.toValuationSubring) :
    ((valuationSubringEquivOfEq v v' h a : v'.toValuationSubring) : F) = (a : F)

def

residueFieldEquivOfEq

L39 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_comp.residueFieldEquivOfEq

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_comp
open AlgebraicCurve

Lean source · statement

def residueFieldEquivOfEq
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v v' : Place K F) (h : v = v') : v.ResidueField ≃+* v'.ResidueField

theorem

pushforwardAlong_comp

L44 ↗

AlgebraicCurve.Divisor.pushforwardAlong_comp

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_comp
open AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Divisor.pushforwardAlong_comp
    {K F F' F'' : Type*} [Field K] [Field F] [Field F'] [Field F'']
    [Algebra K F] [Algebra K F'] [Algebra K F'']
    (φ : F →ₐ[K] F') (ψ : F' →ₐ[K] F'')
    (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral) (hψφ : (ψ.comp
      φ).toRingHom.IsIntegral)
    (D : Divisor K F'') :
    Divisor.pushforwardAlong (ψ.comp φ) hψφ D =
      Divisor.pushforwardAlong φ hφ (Divisor.pushforwardAlong ψ hψ D)

Module documentation

Divisor pushforward Along comp

Declarations

valuationSubringEquivOfEq

coe_valuationSubringEquivOfEq

residueFieldEquivOfEq

pushforwardAlong_comp