Module

SemilinearAut_pic0_correspondence_smul.lean

Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_pic0_correspondence_smul

2 declarations indexed from sourceView source ↗

Module documentation

Semilinear Aut pic0 correspondence smul

Imports2

Imported by1

Nyll.AlgebraicCurves.Divisors.Semilinear.All

theorem

solution

L26 ↗

AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_smul.solution

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_smul
open AlgebraicCurve AlgebraicCurve.SemilinearAut

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'} [HasPrincipalDivisors K F']
    (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (hFI : FundamentalIdentityAlong K φ hφ) (hfin : FiniteAlong K ψ)
    (hN : NormFormulaAlong K ψ hfin)
    (hgφ : IntertwinesAlong φ.toRingHom g g') (hgψ : IntertwinesAlong ψ.toRingHom g g')
    (c : Pic0 K F) :
    Pic0.correspondence φ ψ hφ hψ hFI hfin hN (g • c)
      = g • Pic0.correspondence φ ψ hφ hψ hFI hfin hN c

theorem

pic0_correspondence_smul

L51 ↗

AlgebraicCurve.SemilinearAut.pic0_correspondence_smul