NYLL
Module

CurveModel_baseChange_semilinearAction.lean

Nyll.AlgebraicCurves.Models.CurveModel_baseChange_semilinearAction
2 declarations indexed from sourceView source ↗

Module documentation

Actual coefficient actions on scalar-extension curve models

The coefficient automorphism induces an isomorphism of the actual pullback curve. Transporting this morphism through the chosen curve-model isomorphism supplies its semilinear action on the function field, with the same action on germs and point valuations. No Picard comparison is an input.

The imported function-field and valuation theorem retains its Anthropic FLT provenance in its source. The pullback construction here is an original proof.

Imports7
Imported by2

Declarations

theorem

coefficient_spec_comp

L34 ↗
AlgebraicCurve.CurveModel.coefficient_spec_comp
Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open scoped Pointwise
namespace AlgebraicCurve.CurveModel
Lean source · statement
theorem coefficient_spec_comp
    {K Ω : Type} [Field K] [Field Ω] [Algebra K Ω] (σ : Ω ≃ₐ[K] Ω) :
    Spec.map (CommRingCat.ofHom σ.toRingHom) ≫ specMap K Ω = specMap K Ω
theorem

exists_baseChange_semilinear_action

L46 ↗
AlgebraicCurve.CurveModel.exists_baseChange_semilinear_action
Documentation

A coefficient automorphism acts on the actual scalar-extension curve and its function field. The action fixes the projection to the original curve and retains the induced formulas on germs and on point valuations.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open scoped Pointwise
namespace AlgebraicCurve.CurveModel
Lean source · statement
theorem exists_baseChange_semilinear_action
    {K Ω F : Type} [Field K] [Field Ω] [IsAlgClosed Ω] [Algebra K Ω]
    [Field F] [Algebra Ω F] {C : Scheme} (c : C ⟶ Spec (.of K))
    (M : CurveModel Ω F) (e : M.C ≅ pullback c (specMap K Ω))
    (he : e.hom ≫ pullback.snd c (specMap K Ω) = M.toBase)
    (σ : Ω ≃ₐ[K] Ω) :
    ∃ (θ : M.C ≅ M.C) (g : SemilinearAut Ω F),
      θ.hom ≫ e.hom ≫ pullback.fst c (specMap K Ω) =
        e.hom ≫ pullback.fst c (specMap K Ω) ∧
      θ.hom ≫ M.toBase = M.toBase ≫ Spec.map (CommRingCat.ofHom σ.toRingHom) ∧
      SemilinearAut.baseAut g = σ.toRingEquiv ∧
      (∀ (U : M.C.Opens) [Nonempty (Scheme.Opens.toScheme U)]
        [Nonempty (Scheme.Opens.toScheme (θ.hom ⁻¹ᵁ U))] (t : Γ(M.C, U)),
        g • M.ffEquiv.symm (M.C.germToFunctionField U t) =
          M.ffEquiv.symm (M.C.germToFunctionField (θ.hom ⁻¹ᵁ U) ((θ.hom.app U).hom t))) ∧
      ∀ x y : SchemeHomOver (𝟙 (Spec (.of Ω))) M.toBase,
        y.1 ≫ θ.hom = Spec.map (CommRingCat.ofHom σ.toRingHom) ≫ x.1 →
          M.pointEquivPlace y = g • M.pointEquivPlace x

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.