AlgebraicCurve.Pic0.pushforwardAlongHom_smul
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_pushforwardAlongHom_smul
noncomputable section
open AlgebraicCurve AlgebraicCurve.SemilinearAutLean source · statement
theorem _root_.AlgebraicCurve.Pic0.pushforwardAlongHom_smul
{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)
(hfin : FiniteAlong K φ) (hN : NormFormulaAlong K φ hfin)
(hgg' : IntertwinesAlong φ.toRingHom g g') (x : Pic0 K F') :
Pic0.pushforwardAlongHom φ hφ hfin hN (g' • x) =
g • Pic0.pushforwardAlongHom φ hφ hfin hN x