Module

SemilinearAut_pullback_smul.lean

Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_pullback_smul

2 declarations indexed from sourceView source ↗

Module documentation

Semilinear Aut pullback smul

Imports3

Imported by2

theorem

solution

L30 ↗

AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pullback_smul.solution

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pullback_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']
  [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] {g : SemilinearAut K F} {g' :
  SemilinearAut K F'} [HasPrincipalDivisors K F'] (hgg' : IntertwinesAlong (algebraMap F F') g g')
  (D : Divisor K F) : Divisor.pullback F' (g • D) = g' • Divisor.pullback F' D

theorem

pullback_smul

L45 ↗

AlgebraicCurve.SemilinearAut.pullback_smul

Source context 1 command