Module

SemilinearAut_pushforwardAlong_smul.lean

Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_pushforwardAlong_smul

2 declarations indexed from sourceView source ↗

Module documentation

Semilinear Aut pushforward Along smul

Imports2

Imported by3

theorem

solution

L29 ↗

AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pushforwardAlong_smul.solution

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pushforwardAlong_smul
open AlgebraicCurve AlgebraicCurve.SemilinearAut
open scoped Pointwise
noncomputable section

Lean source · statement

theorem solution {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] {g :
  SemilinearAut K F} {g' : SemilinearAut K F'} (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hgg'
  : IntertwinesAlong φ.toRingHom g g') (D : Divisor K F') : Divisor.pushforwardAlong φ hφ (g' • D)
  = g • Divisor.pushforwardAlong φ hφ D

theorem

pushforwardAlong_smul

L45 ↗

AlgebraicCurve.SemilinearAut.pushforwardAlong_smul

Source context 1 command