Module

ConstantExtensionFixedDivisors.lean

Nyll.JacobianVarieties.Picard.ConstantExtensionFixedDivisors

2 declarations indexed from sourceView source ↗

Module documentation

Constant-extension divisors are fixed by coefficient actions

Uniqueness of the actual lifted valuation implies that an action fixing the old function field fixes each lifted old place, and hence its conorm divisors. The fixed-function-field input is supplied by the geometric projection square in CurveModel.semilinear_fixes_functionField_image.

Imports2

Imported by2

theorem

constantExtension_place_fixed

L47 ↗

JacobianVarieties.Picard.constantExtension_place_fixed

Documentation

Coefficient actions fix the unique extension of each original place.

Source context 8 commands

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

noncomputable section
open AlgebraicCurve
open JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc
open scoped Pointwise
namespace JacobianVarieties.Picard
attribute [local instance]
  AlgebraicCurve.SemilinearAut.instMulSemiringActionSubtypeProdRingAutMemSubgroup
  AlgebraicCurve.SemilinearAut.instMulActionSubtypeProdRingAutMemSubgroupPlace
  AlgebraicCurve.SemilinearAut.instDistribMulActionSubtypeProdRingAutMemSubgroupDivisor
variable {K F K' F' : Type*}
  [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  [IsAlgClosed K] [IsCurveOver K F]
  (hfg : ∃ x : F, Transcendental K x ∧
    FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
  (hfg' : ∃ x : F', Transcendental K' x ∧
    FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
  (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
  (σ : SemilinearAut K' F')
  (hfix : ∀ f : F, σ • algebraMap F F' f = algebraMap F F' f)
include hfix in

Lean source · statement

theorem constantExtension_place_fixed (v : Place K F) :
    σ • lift hfg hfg' hgen v = lift hfg hfg' hgen v

theorem

constantExtension_divisor_fixed

L64 ↗

JacobianVarieties.Picard.constantExtension_divisor_fixed