Module

CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.lean

Nyll.AlgebraicCurves.Models.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul

26 declarations indexed from sourceView source ↗

Module documentation

Curve Model exists semilinear Aut base Aut eq and point Equiv Place eq smul

Imports2

Imported by3

def

pull

L47 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.pull

Documentation

Pull a function-field element back through the specialization of generic points.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}

Lean source · statement

def pull [IrreducibleSpace X] [IrreducibleSpace Y] (f : X ⟶ Y)
    (h : f.base (genericPoint X) ⤳ genericPoint Y) : Y.functionField ⟶ X.functionField

theorem

pull_germ

L55 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.pull_germ

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
section
variable [IrreducibleSpace X] [IrreducibleSpace Y] [IrreducibleSpace Z]

Lean source · statement

theorem pull_germ (f : X ⟶ Y) (h : f.base (genericPoint X) ⤳ genericPoint Y)
    (U : Y.Opens) (hU : genericPoint Y ∈ U) (s : Γ(Y, U)) :
    pull f h (Y.presheaf.germ U (genericPoint Y) hU s) =
      X.presheaf.germ (f ⁻¹ᵁ U) (genericPoint X) (h.mem_open U.isOpen hU) (f.app U s)

theorem

pull_algebraMap

L62 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.pull_algebraMap

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
section
variable [IrreducibleSpace X] [IrreducibleSpace Y] [IrreducibleSpace Z]

Lean source · statement

theorem pull_algebraMap (f : X ⟶ Y) (h : f.base (genericPoint X) ⤳ genericPoint Y) (x : X)
    (a : Y.presheaf.stalk (f.base x)) :
    pull f h (algebraMap (Y.presheaf.stalk (f.base x)) Y.functionField a) =
      algebraMap (X.presheaf.stalk x) X.functionField (f.stalkMap x a)

theorem

pull_id

L72 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.pull_id

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
section
variable [IrreducibleSpace X] [IrreducibleSpace Y] [IrreducibleSpace Z]

Lean source · statement

theorem pull_id : pull (𝟙 X) (specializes_refl _) = 𝟙 _

theorem

pull_comp

L75 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.pull_comp

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
section
variable [IrreducibleSpace X] [IrreducibleSpace Y] [IrreducibleSpace Z]

Lean source · statement

theorem pull_comp (f : X ⟶ Y) (g : Y ⟶ Z) (hf : f.base (genericPoint X) ⤳ genericPoint Y)
    (hg : g.base (genericPoint Y) ⤳ genericPoint Z) :
    pull (f ≫ g) ((g.base.hom.map_specializes hf).trans hg) = pull g hg ≫ pull f hf

theorem

specializes_of_iso

L87 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.specializes_of_iso

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem specializes_of_iso (e : X ≅ Y) : e.hom.base (genericPoint X) ⤳ genericPoint Y

theorem

specializes_of_iso_inv

L90 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.specializes_of_iso_inv

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem specializes_of_iso_inv (e : X ≅ Y) : e.inv.base (genericPoint Y) ⤳ genericPoint X

def

equivOfIso

L94 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.equivOfIso

Documentation

The function-field equivalence induced by an isomorphism of integral schemes.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

def equivOfIso (e : X ≅ Y) : Y.functionField ≃+* X.functionField

theorem

equivOfIso_apply

L112 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.equivOfIso_apply

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem equivOfIso_apply (e : X ≅ Y) (a : Y.functionField) :
    equivOfIso e a = pull e.hom (specializes_of_iso e) a

theorem

equivOfIso_symm_apply

L115 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.equivOfIso_symm_apply

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem equivOfIso_symm_apply (e : X ≅ Y) (a : X.functionField) :
    (equivOfIso e).symm a = pull e.inv (specializes_of_iso_inv e) a

theorem

map_equivOfIso_range_stalk

L118 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.map_equivOfIso_range_stalk

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem map_equivOfIso_range_stalk (e : X ≅ Y) (x : X) :
    (algebraMap (Y.presheaf.stalk (e.hom.base x)) Y.functionField).range.map
        (equivOfIso e).toRingHom =
      (algebraMap (X.presheaf.stalk x) X.functionField).range

theorem

image_equivOfIso_range_stalk

L134 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.image_equivOfIso_range_stalk

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem image_equivOfIso_range_stalk (e : X ≅ Y) (x : X) :
    (equivOfIso e) ''
        ((algebraMap (Y.presheaf.stalk (e.hom.base x)) Y.functionField).range : Set _) =
      ((algebraMap (X.presheaf.stalk x) X.functionField).range : Set _)

theorem

image_equivOfIso_symm_range_stalk

L142 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.image_equivOfIso_symm_range_stalk

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem image_equivOfIso_symm_range_stalk (e : X ≅ Y) (x : X) :
    (equivOfIso e).symm '' ((algebraMap (X.presheaf.stalk x) X.functionField).range : Set _) =
      ((algebraMap (Y.presheaf.stalk (e.hom.base x)) Y.functionField).range : Set _)

theorem

pull_baseToFunctionField

L148 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.pull_baseToFunctionField

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem pull_baseToFunctionField {K : Type u} [Field K] (f : X ⟶ Y)
    (h : f.base (genericPoint X) ⤳ genericPoint Y)
    (cX : X ⟶ Spec (CommRingCat.of K)) (cY : Y ⟶ Spec (CommRingCat.of K)) (hf : f ≫ cY = cX)
    (a : K) :
    pull f h (baseToFunctionField cY a) = baseToFunctionField cX a

theorem

equivOfIso_baseToFunctionField

L160 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.FunctionFieldPull.equivOfIso_baseToFunctionField

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
namespace FunctionFieldPull
variable {X Y Z : Scheme.{u}}
variable [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem equivOfIso_baseToFunctionField {K : Type u} [Field K] (e : X ≅ Y)
    (cX : X ⟶ Spec (CommRingCat.of K)) (cY : Y ⟶ Spec (CommRingCat.of K))
    (hf : e.hom ≫ cY = cX) (a : K) :
    equivOfIso e (baseToFunctionField cY a) = baseToFunctionField cX a

theorem

pull_baseToFunctionField_twist

L174 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.pull_baseToFunctionField_twist

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
open FunctionFieldPull
section
variable {X Y : Scheme.{u}} [IrreducibleSpace X] [IrreducibleSpace Y] [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem pull_baseToFunctionField_twist {K : Type u} [Field K] (f : X ⟶ Y)
    (h : f.base (genericPoint X) ⤳ genericPoint Y)
    (cX : X ⟶ Spec (CommRingCat.of K)) (cY : Y ⟶ Spec (CommRingCat.of K)) (τ : K ≃+* K)
    (hf : f ≫ cY = cX ≫ Spec.map (CommRingCat.ofHom (τ : K →+* K))) (a : K) :
    pull f h (baseToFunctionField cY a) = baseToFunctionField cX (τ a)

def

gRingEquiv

L202 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.gRingEquiv

Documentation

The function-field ring automorphism induced by an automorphism of the curve model.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
open FunctionFieldPull
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

def gRingEquiv (M : CurveModel K L) (e : M.C ≅ M.C) : L ≃+* L

theorem

gRingEquiv_apply

L205 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.gRingEquiv_apply

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
open FunctionFieldPull
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem gRingEquiv_apply (M : CurveModel K L) (e : M.C ≅ M.C) (a : L) :
    gRingEquiv M e a = M.ffEquiv.symm (equivOfIso e (M.ffEquiv a))

theorem

gRingEquiv_algebraMap

L208 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.gRingEquiv_algebraMap

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
open FunctionFieldPull
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem gRingEquiv_algebraMap (M : CurveModel K L) (e : M.C ≅ M.C) (τ : K ≃+* K)
    (he : e.hom ≫ M.toBase = M.toBase ≫ Spec.map (CommRingCat.ofHom (τ : K →+* K))) (a : K) :
    gRingEquiv M e (algebraMap K L a) = algebraMap K L (τ a)

def

gSL

L217 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.gSL

Documentation

The semilinear function-field automorphism induced by a scheme automorphism over a base automorphism.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
open FunctionFieldPull
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

def gSL (M : CurveModel K L) (e : M.C ≅ M.C) (τ : K ≃+* K)
    (he : e.hom ≫ M.toBase = M.toBase ≫ Spec.map (CommRingCat.ofHom (τ : K →+* K))) : SemilinearAut
      K L

theorem

gSL_smul

L222 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.gSL_smul

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
open FunctionFieldPull
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem gSL_smul (M : CurveModel K L) (e : M.C ≅ M.C) (τ : K ≃+* K)
    (he : e.hom ≫ M.toBase = M.toBase ≫ Spec.map (CommRingCat.ofHom (τ : K →+* K))) (a : L) :
    gSL M e τ he • a = M.ffEquiv.symm (equivOfIso e (M.ffEquiv a))

theorem

baseAut_gSL

L226 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.baseAut_gSL

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
open FunctionFieldPull
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem baseAut_gSL (M : CurveModel K L) (e : M.C ≅ M.C) (τ : K ≃+* K)
    (he : e.hom ≫ M.toBase = M.toBase ≫ Spec.map (CommRingCat.ofHom (τ : K →+* K))) :
    SemilinearAut.baseAut (gSL M e τ he) = τ

theorem

germ_clause

L230 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.germ_clause

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
open FunctionFieldPull
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem germ_clause (M : CurveModel K L) (e : M.C ≅ M.C) (τ : K ≃+* K)
    (he : e.hom ≫ M.toBase = M.toBase ≫ Spec.map (CommRingCat.ofHom (τ : K →+* K)))
    (U : M.C.Opens) [Nonempty (Scheme.Opens.toScheme U)] [Nonempty (Scheme.Opens.toScheme (e.hom
      ⁻¹ᵁ U))]
    (t : Γ(M.C, U)) :
    gSL M e τ he • M.ffEquiv.symm (M.C.germToFunctionField U t) =
      M.ffEquiv.symm (M.C.germToFunctionField (e.hom ⁻¹ᵁ U) ((e.hom.app U).hom t))

theorem

coe_toValuationSubring_pointEquivPlace

L241 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.coe_toValuationSubring_pointEquivPlace

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
open FunctionFieldPull
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem coe_toValuationSubring_pointEquivPlace [IsAlgClosed K] (M : CurveModel K L)
    (x : {q : Spec (CommRingCat.of K) ⟶ M.C // q ≫ M.toBase = 𝟙 _}) :
    ((M.pointEquivPlace x).toValuationSubring : Set L) =
      M.ffEquiv.symm '' ((algebraMap (M.C.presheaf.stalk (x.1.base (IsLocalRing.closedPoint K)))
        M.C.functionField).range : Set M.C.functionField)

theorem

point_clause

L253 ↗

AlgebraicCurves.Models.Proofs.CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul.AlgebraicCurve.CurveModel.GalPtSol.point_clause

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace GalPtSol
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
open FunctionFieldPull
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem point_clause [IsAlgClosed K] (M : CurveModel K L) (e : M.C ≅ M.C) (τ : K ≃+* K)
    (he : e.hom ≫ M.toBase = M.toBase ≫ Spec.map (CommRingCat.ofHom (τ : K →+* K)))
    (x y : {p : Spec (CommRingCat.of K) ⟶ M.C // p ≫ M.toBase = 𝟙 _})
    (hxy : y.1 ≫ e.hom = Spec.map (CommRingCat.ofHom (τ : K →+* K)) ≫ x.1) :
    M.pointEquivPlace y = gSL M e τ he • M.pointEquivPlace x

theorem

exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul

L285 ↗

AlgebraicCurve.CurveModel.exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
open AlgebraicCurve.CurveModel.GalPtSol in

Lean source · statement

theorem _root_.AlgebraicCurve.CurveModel.exists_semilinearAut_baseAut_eq_and_pointEquivPlace_eq_smul
    {K : Type u} [Field K] [IsAlgClosed K] {L : Type v} [Field L] [Algebra K L]
    (M : AlgebraicCurve.CurveModel K L) (τ : K ≃+* K) (h : M.C ⟶ M.C) [IsIso h]
    (hh : h ≫ M.toBase = M.toBase ≫ Spec.map (CommRingCat.ofHom (τ : K →+* K))) :
    ∃ g : AlgebraicCurve.SemilinearAut K L,
      AlgebraicCurve.SemilinearAut.baseAut g = τ ∧
      (∀ (U : M.C.Opens) [Nonempty (Scheme.Opens.toScheme U)] [Nonempty (Scheme.Opens.toScheme (h
        ⁻¹ᵁ U))]
        (t : Γ(M.C, U)),
        g • M.ffEquiv.symm (M.C.germToFunctionField U t) =
          M.ffEquiv.symm (M.C.germToFunctionField (h ⁻¹ᵁ U) ((h.app U).hom t))) ∧
      ∀ x y : {p : Spec (CommRingCat.of K) ⟶ M.C // p ≫ M.toBase = 𝟙 _},
        y.1 ≫ h = Spec.map (CommRingCat.ofHom (τ : K →+* K)) ≫ x.1 →
          M.pointEquivPlace y = g • M.pointEquivPlace x

Module documentation

Curve Model exists semilinear Aut base Aut eq and point Equiv Place eq smul

Declarations