Module

Divisor_pushforwardAlong_pullbackAlong_of_surjective.lean

Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardAlong_pullbackAlong_of_surjective

4 declarations indexed from sourceView source ↗

Module documentation

Divisor pushforward Along pullback Along of surjective

Imports3

Imported by4

theorem

separableAlong_of_surjective_aux

L31 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_pullbackAlong_of_surjective.separableAlong_of_surjective_aux

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_pullbackAlong_of_surjective
open _root_.AlgebraicCurve
section Helpers
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · statement

theorem separableAlong_of_surjective_aux (φ : F →ₐ[K] F') (hs : Function.Surjective φ) :
    SeparableAlong K φ

theorem

finrankAlong_eq_one_of_surjective_aux

L38 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_pullbackAlong_of_surjective.finrankAlong_eq_one_of_surjective_aux

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_pullbackAlong_of_surjective
open _root_.AlgebraicCurve
section Helpers
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · statement

theorem finrankAlong_eq_one_of_surjective_aux (φ : F →ₐ[K] F') (hs : Function.Surjective φ)
  :
    finrankAlong K φ = 1

theorem

pushforwardAlong_pullbackAlong_of_surjective_aux

L55 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_pullbackAlong_of_surjective.AlgebraicCurve.Divisor.pushforwardAlong_pullbackAlong_of_surjective_aux

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_pullbackAlong_of_surjective
open _root_.AlgebraicCurve
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Divisor in

Lean source · statement

theorem AlgebraicCurve.Divisor.pushforwardAlong_pullbackAlong_of_surjective_aux {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) (hs : Function.Surjective φ) (D :
  AlgebraicCurve.Divisor K F) : AlgebraicCurve.Divisor.pushforwardAlong φ hφ
  (AlgebraicCurve.Divisor.pullbackAlong φ hφ D) = D

theorem

pushforwardAlong_pullbackAlong_of_surjective

L80 ↗

AlgebraicCurve.Divisor.pushforwardAlong_pullbackAlong_of_surjective

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_pullbackAlong_of_surjective
open _root_.AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Divisor.pushforwardAlong_pullbackAlong_of_surjective {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) (hs : Function.Surjective φ) (D : AlgebraicCurve.Divisor
  K F) : AlgebraicCurve.Divisor.pushforwardAlong φ hφ (AlgebraicCurve.Divisor.pullbackAlong φ hφ D)
  = D

Module documentation

Divisor pushforward Along pullback Along of surjective

Declarations

separableAlong_of_surjective_aux

finrankAlong_eq_one_of_surjective_aux

pushforwardAlong_pullbackAlong_of_surjective_aux

pushforwardAlong_pullbackAlong_of_surjective