Module

CurveModelSemilinearFixedField.lean

Nyll.AlgebraicCurves.Models.CurveModelSemilinearFixedField

2 declarations indexed from sourceView source ↗

Module documentation

The original function field is fixed by coefficient actions

If a geometric coefficient automorphism fixes the projection to the original curve, its actual semilinear function-field action fixes every function coming from that curve. The proof uses the action on germs and the actual commutative square, not a fixed-field assumption.

Imports2

Imported by3

theorem

semilinear_fixes_functionField_image

L32 ↗

AlgebraicCurve.CurveModel.semilinear_fixes_functionField_image

Documentation

The geometric projection square and germ formulas force the semilinear action to fix the original function-field image.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped Pointwise
namespace AlgebraicCurve.CurveModel
attribute [local instance]
  AlgebraicCurve.SemilinearAut.instMulSemiringActionSubtypeProdRingAutMemSubgroup
  AlgebraicCurve.SemilinearAut.instMulActionSubtypeProdRingAutMemSubgroupPlace

Lean source · statement

theorem semilinear_fixes_functionField_image
    {K F : Type} [Field K] [Field F] [Algebra K F]
    (M : CurveModel K F) {X : Scheme} [IsIntegral X]
    (p : M.C ⟶ X) (hp : p.base (genericPoint M.C) = genericPoint X)
    (φ : X.functionField →+* F) (θ : M.C ≅ M.C)
    (hθ : θ.hom ≫ p = p) (g : SemilinearAut K F)
    (hφ : ∀ (U : X.Opens) [Nonempty U] [Nonempty (p ⁻¹ᵁ U)] (s : Γ(X, U)),
      φ (X.germToFunctionField U s) =
        M.ffEquiv.symm (M.C.germToFunctionField (p ⁻¹ᵁ U) ((p.app U).hom s)))
    (hg : ∀ (V : M.C.Opens) [Nonempty V] [Nonempty (θ.hom ⁻¹ᵁ V)]
      (t : Γ(M.C, V)),
      g • M.ffEquiv.symm (M.C.germToFunctionField V t) =
        M.ffEquiv.symm (M.C.germToFunctionField (θ.hom ⁻¹ᵁ V)
          ((θ.hom.app V).hom t)))
    (r : X.functionField) :
    g • φ r = φ r

theorem

point_fixed_of_projection_fixed

L77 ↗

AlgebraicCurve.CurveModel.point_fixed_of_projection_fixed