NYLL
Module

CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.lean

Nyll.AlgebraicCurves.Models.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
23 declarations indexed from sourceView source ↗

Module documentation

Curve Model exists alg Equiv point Equiv Place comp hom eq of Alg Aut smul point Equiv

Place

Imports2
Imported by1

Declarations

def

pull

L48 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L56 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L63 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L73 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L76 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L88 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L91 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L95 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L113 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L116 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L119 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L135 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L143 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L149 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

L161 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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
def

tauRingEquiv

L174 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.tauRingEquiv
Documentation

The ring automorphism of the modeled field induced by an isomorphism of curve models.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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 tauRingEquiv (M M' : CurveModel K L) (e : M.C ≅ M'.C) : L ≃+* L
theorem

tauRingEquiv_apply

L177 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.tauRingEquiv_apply
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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 tauRingEquiv_apply (M M' : CurveModel K L) (e : M.C ≅ M'.C) (a : L) :
    tauRingEquiv M M' e a = M'.ffEquiv.symm ((equivOfIso e).symm (M.ffEquiv a))
theorem

tauRingEquiv_algebraMap

L180 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.tauRingEquiv_algebraMap
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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 tauRingEquiv_algebraMap (M M' : CurveModel K L) (e : M.C ≅ M'.C)
    (he : e.hom ≫ M'.toBase = M.toBase) (a : K) :
    tauRingEquiv M M' e (algebraMap K L a) = algebraMap K L a
def

tau

L189 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.tau
Documentation

The base-field algebra automorphism induced by an isomorphism of curve models over the base.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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 tau (M M' : CurveModel K L) (e : M.C ≅ M'.C) (he : e.hom ≫ M'.toBase = M.toBase) :
    L ≃ₐ[K] L
theorem

tau_apply

L193 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.tau_apply
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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 tau_apply (M M' : CurveModel K L) (e : M.C ≅ M'.C) (he : e.hom ≫ M'.toBase = M.toBase)
    (a : L) : tau M M' e he a = M'.ffEquiv.symm ((equivOfIso e).symm (M.ffEquiv a))
theorem

coe_toValuationSubring_pointEquivPlace

L196 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.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_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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

pointEquivPlace_comp_eq_smul

L208 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace.AlgebraicCurve.CurveModel.ModelIndepSol.pointEquivPlace_comp_eq_smul
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
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 ModelIndepSol
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 · full declaration
theorem pointEquivPlace_comp_eq_smul [IsAlgClosed K] (M M' : CurveModel K L) (e : M.C ≅ M'.C)
    (he : e.hom ≫ M'.toBase = M.toBase)
    (x : {p : Spec (CommRingCat.of K) ⟶ M.C // p ≫ M.toBase = 𝟙 _}) :
    M'.pointEquivPlace ⟨x.1 ≫ e.hom, by rw [Category.assoc, he]; exact x.2⟩ =
      SemilinearAut.ofAlgAut (tau M M' e he) • M.pointEquivPlace x := by
  apply Place.ext
  apply SetLike.coe_injective
  rw [SemilinearAut.smul_toValuationSubring, ValuationSubring.coe_pointwise_smul, ← Set.image_smul,
    coe_toValuationSubring_pointEquivPlace, coe_toValuationSubring_pointEquivPlace]
  change M'.ffEquiv.symm '' ((algebraMap (M'.C.presheaf.stalk
      (e.hom.base (x.1.base (IsLocalRing.closedPoint K)))) M'.C.functionField).range : Set _) = _
  simp only [SemilinearAut.ofAlgAut_smul]
  rw [← Set.image_comp]
  have hcomp : ((fun m => tau M M' e he m) ∘ (M.ffEquiv.symm : M.C.functionField → L)) =
      (M'.ffEquiv.symm : M'.C.functionField → L) ∘ ((equivOfIso e).symm) := by
    funext a
    simp [Function.comp_apply, tau_apply]
  rw [hcomp, Set.image_comp, image_equivOfIso_symm_range_stalk]
theorem

exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace

L244 ↗
AlgebraicCurve.CurveModel.exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurve
universe u v
open _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.AlgebraicCurves.Models.Proofs in
open CurveModel_exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace in
open AlgebraicCurve.CurveModel.ModelIndepSol in
Lean source · full declaration
theorem CurveModel.exists_algEquiv_pointEquivPlace_comp_hom_eq_ofAlgAut_smul_pointEquivPlace
    (K : Type u) [Field K] [IsAlgClosed K] (L : Type v) [Field L] [Algebra K L]
    (M M' : AlgebraicCurve.CurveModel K L) (e : M.C ≅ M'.C) (he : e.hom ≫ M'.toBase = M.toBase) :
    ∃ τ : L ≃ₐ[K] L,
      ∀ x : {p : Spec (CommRingCat.of K) ⟶ M.C // p ≫ M.toBase = 𝟙 _},
        M'.pointEquivPlace ⟨x.1 ≫ e.hom, by rw [Category.assoc, he]; exact x.2⟩ =
          SemilinearAut.ofAlgAut τ • M.pointEquivPlace x :=
  ⟨tau M M' e he, fun x => pointEquivPlace_comp_eq_smul M M' e he x⟩

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