Module

Divisor_pullbackAlong_pullbackAlong.lean

Nyll.AlgebraicCurves.Divisors.Divisor_pullbackAlong_pullbackAlong

1 declaration indexed from sourceView source ↗

Module documentation

Divisor pullback Along pullback Along

Imports3

Imported by5

theorem

pullbackAlong_pullbackAlong

L27 ↗

AlgebraicCurve.Divisor.pullbackAlong_pullbackAlong

Source context 3 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Divisor.pullbackAlong_pullbackAlong {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'') [HasPrincipalDivisors K F'] [HasPrincipalDivisors K F''] (hφ :
  φ.toRingHom.IsIntegral) (hχ : χ.toRingHom.IsIntegral) (hχφ : (χ.comp φ).toRingHom.IsIntegral) (D
  : Divisor K F) : Divisor.pullbackAlong χ hχ (Divisor.pullbackAlong φ hφ D) =
  Divisor.pullbackAlong (χ.comp φ) hχφ D

Module documentation

Divisor pullback Along pullback Along

Declarations

pullbackAlong_pullbackAlong