Module

Divisor_pushforwardAlong_pushforwardAlong.lean

Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardAlong_pushforwardAlong

1 declaration indexed from sourceView source ↗

Module documentation

Divisor pushforward Along pushforward Along

Imports3

Imported by5

theorem

pushforwardAlong_pushforwardAlong

L28 ↗

AlgebraicCurve.Divisor.pushforwardAlong_pushforwardAlong

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_pushforwardAlong
open IsDedekindDomain AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Divisor.pushforwardAlong_pushforwardAlong {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 φ hφ
  (Divisor.pushforwardAlong χ hχ D) = Divisor.pushforwardAlong (χ.comp φ) hχφ D

Module documentation

Divisor pushforward Along pushforward Along

Declarations

pushforwardAlong_pushforwardAlong