NYLL
Module

CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.lean

Nyll.AlgebraicCurves.Models.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
34 declarations indexed from sourceView source ↗

Module documentation

Curve Model ff Equiv symm stalk Map eq algebra Map

Imports4
Imported by2

Declarations

theorem

ord_nonneg_of_mem

L35 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.ord_nonneg_of_mem
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem ord_nonneg_of_mem (v : Place K L) {f : L} (hf : f ∈ v.toValuationSubring) :
    0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L51 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.mem_of_ord_nonneg
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem mem_of_ord_nonneg (v : Place K L) {f : L} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring
theorem

ord_coe_eq_zero_iff_isUnit

L59 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.ord_coe_eq_zero_iff_isUnit
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem ord_coe_eq_zero_iff_isUnit (v : Place K L) (a : v.toValuationSubring) (ha : (a : L) ≠ 0) :
    v.ord (a : L) = 0 ↔ IsUnit a
theorem

mem_maximalIdeal_iff_ord_pos

L71 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.mem_maximalIdeal_iff_ord_pos
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem mem_maximalIdeal_iff_ord_pos (v : Place K L) (a : v.toValuationSubring) (ha : (a : L) ≠ 0) :
    a ∈ maximalIdeal v.toValuationSubring ↔ 0 < v.ord (a : L)
def

VanishesAt

L78 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.VanishesAt
Documentation

The function belongs to the valuation subring and its residue at the place is zero.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
def VanishesAt (w : Place K L) (z : L) : Prop
theorem

sub

L82 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.VanishesAt.sub
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem VanishesAt.sub {w : Place K L} {a b : L} (ha : VanishesAt w a) (hb : VanishesAt w b) :
    VanishesAt w (a - b)
theorem

vanishesAt_zero

L88 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.vanishesAt_zero
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem vanishesAt_zero (w : Place K L) : VanishesAt w (0 : L)
theorem

vanishesAt_of_mem_maximalIdeal

L94 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.vanishesAt_of_mem_maximalIdeal
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem vanishesAt_of_mem_maximalIdeal {w : Place K L} {a : w.toValuationSubring}
    (ha : a ∈ maximalIdeal w.toValuationSubring) : VanishesAt w (a : L)
theorem

vanishesAt_of_ord_pos

L98 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.vanishesAt_of_ord_pos
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem vanishesAt_of_ord_pos {w : Place K L} {z : L} (hz : 0 < w.ord z) : VanishesAt w z
theorem

eq_zero_or_ord_pos

L104 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.VanishesAt.eq_zero_or_ord_pos
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem VanishesAt.eq_zero_or_ord_pos {w : Place K L} {z : L} (h : VanishesAt w z) :
    z = 0 ∨ 0 < w.ord z
theorem

finite_setOf_ord_ne_zero

L111 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.finite_setOf_ord_ne_zero
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem finite_setOf_ord_ne_zero [HasPrincipalDivisors K L] {g : L} (hg : g ≠ 0) :
    {w : Place K L | w.ord g ≠ 0}.Finite
theorem

exists_sub_algebraMap_mem_maximalIdeal

L118 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.exists_sub_algebraMap_mem_maximalIdeal
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exists_sub_algebraMap_mem_maximalIdeal [IsAlgClosed K] (v : Place K L)
    [Module.Finite K v.ResidueField] (a : v.toValuationSubring) :
    ∃ c : K, a - algebraMap K v.toValuationSubring c ∈ maximalIdeal v.toValuationSubring
theorem

exists_ord_pos_of_ord_neg

L129 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.exists_ord_pos_of_ord_neg
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exists_ord_pos_of_ord_neg [IsAlgClosed K] [IsCurveOver K L] {g : L} (hg : g ≠ 0)
    {w₀ : Place K L} (hneg : w₀.ord g < 0) : ∃ w : Place K L, 0 < w.ord g
theorem

infinite_place

L151 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.infinite_place
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem infinite_place [IsAlgClosed K] [IsCurveOver K L] (w₀ : Place K L) : Infinite (Place K L)
theorem

eq_zero_of_vanishesAt_off_finite

L188 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.eq_zero_of_vanishesAt_off_finite
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem eq_zero_of_vanishesAt_off_finite [IsAlgClosed K] [IsCurveOver K L] [Nonempty (Place K L)]
    {g : L} (S : Set (Place K L)) (hS : S.Finite) (h : ∀ w, w ∉ S → VanishesAt w g) : g = 0
theorem

mem_maximalIdeal_iff_of_ringEquiv

L201 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.mem_maximalIdeal_iff_of_ringEquiv
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section FieldSide
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem mem_maximalIdeal_iff_of_ringEquiv {R S : Type*} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] (e : R ≃+* S) (x : R) :
    x ∈ maximalIdeal R ↔ e x ∈ maximalIdeal S
def

stalkToField

L220 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.stalkToField
Documentation

The homomorphism from a stalk to the modeled function field.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section ModelSide
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
def stalkToField (M : CurveModel K L) (z : M.C) : M.C.presheaf.stalk z →+* L
theorem

stalkToField_apply

L224 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.stalkToField_apply
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section ModelSide
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
theorem stalkToField_apply (M : CurveModel K L) (z : M.C) (s : M.C.presheaf.stalk z) :
    stalkToField M z s = M.ffEquiv.symm (algebraMap (M.C.presheaf.stalk z) M.C.functionField s)
theorem

stalkToField_injective

L228 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.stalkToField_injective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section ModelSide
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
theorem stalkToField_injective (M : CurveModel K L) (z : M.C) : Function.Injective (stalkToField M
  z)
def

stalkEquivOfRange

L233 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.stalkEquivOfRange
Documentation

The stalk equivalence with a valuation ring having the same image in the function field.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section ModelSide
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
def stalkEquivOfRange (M : CurveModel K L) (z : M.C) (P : Place K L)
    (hr : (stalkToField M z).range = P.toValuationSubring.toSubring) :
    M.C.presheaf.stalk z ≃+* P.toValuationSubring
theorem

coe_stalkEquivOfRange

L246 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.coe_stalkEquivOfRange
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section ModelSide
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
theorem coe_stalkEquivOfRange (M : CurveModel K L) (z : M.C) (P : Place K L)
    (hr : (stalkToField M z).range = P.toValuationSubring.toSubring) (s : M.C.presheaf.stalk z) :
    ((stalkEquivOfRange M z P hr s : P.toValuationSubring) : L) = stalkToField M z s
theorem

nonempty_place

L250 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.nonempty_place
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section ModelSide
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
theorem nonempty_place [IsAlgClosed K] (M : CurveModel K L) : Nonempty (Place K L)
def

psi

L281 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.psi
Documentation

The homomorphism of modeled fields obtained by conjugating the scheme function-field map.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section Rigidity
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v
variable {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F']
  [Algebra k F] [Algebra k F']
  [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
  [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
  (M : CurveModel k F) (M' : CurveModel k F')
  (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
  (φ : M.C.functionField →+* M'.C.functionField)
  (hφk : ∀ a : k, φ (baseToFunctionField M.toBase a) = baseToFunctionField M'.toBase a)
  (hφnat : ∀ (p : M'.C) (s : M.C.presheaf.stalk (π.base p)),
    algebraMap _ M'.C.functionField (π.stalkMap p s) = φ (algebraMap _ M.C.functionField s))
Lean source · statement
def psi : F →+* F'
theorem

psi_apply

L286 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.psi_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section Rigidity
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v
variable {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F']
  [Algebra k F] [Algebra k F']
  [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
  [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
  (M : CurveModel k F) (M' : CurveModel k F')
  (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
  (φ : M.C.functionField →+* M'.C.functionField)
  (hφk : ∀ a : k, φ (baseToFunctionField M.toBase a) = baseToFunctionField M'.toBase a)
  (hφnat : ∀ (p : M'.C) (s : M.C.presheaf.stalk (π.base p)),
    algebraMap _ M'.C.functionField (π.stalkMap p s) = φ (algebraMap _ M.C.functionField s))
omit [IsAlgClosed k] [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F]
  [Algebra.EssFiniteType k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] in
Lean source · statement
theorem psi_apply (f : F) : psi M M' φ f = M'.ffEquiv.symm (φ (M.ffEquiv f))
theorem

psi_algebraMap

L290 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.psi_algebraMap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section Rigidity
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v
variable {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F']
  [Algebra k F] [Algebra k F']
  [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
  [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
  (M : CurveModel k F) (M' : CurveModel k F')
  (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
  (φ : M.C.functionField →+* M'.C.functionField)
  (hφk : ∀ a : k, φ (baseToFunctionField M.toBase a) = baseToFunctionField M'.toBase a)
  (hφnat : ∀ (p : M'.C) (s : M.C.presheaf.stalk (π.base p)),
    algebraMap _ M'.C.functionField (π.stalkMap p s) = φ (algebraMap _ M.C.functionField s))
include hφk in
omit [IsAlgClosed k] [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F]
  [Algebra.EssFiniteType k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] in
Lean source · statement
theorem psi_algebraMap (c : k) : psi M M' φ (algebraMap k F c) = algebraMap k F' c
theorem

stalkToField_stalkMap

L295 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.stalkToField_stalkMap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section Rigidity
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v
variable {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F']
  [Algebra k F] [Algebra k F']
  [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
  [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
  (M : CurveModel k F) (M' : CurveModel k F')
  (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
  (φ : M.C.functionField →+* M'.C.functionField)
  (hφk : ∀ a : k, φ (baseToFunctionField M.toBase a) = baseToFunctionField M'.toBase a)
  (hφnat : ∀ (p : M'.C) (s : M.C.presheaf.stalk (π.base p)),
    algebraMap _ M'.C.functionField (π.stalkMap p s) = φ (algebraMap _ M.C.functionField s))
include hφnat in
omit [IsAlgClosed k] [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F]
  [Algebra.EssFiniteType k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] in
Lean source · statement
theorem stalkToField_stalkMap (p : M'.C) (s : M.C.presheaf.stalk (π.base p)) :
    stalkToField M' p (π.stalkMap p s) = psi M M' φ (stalkToField M (π.base p) s)
theorem

vanishesAt_psi_sub

L300 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.vanishesAt_psi_sub
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section Rigidity
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v
variable {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F']
  [Algebra k F] [Algebra k F']
  [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
  [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
  (M : CurveModel k F) (M' : CurveModel k F')
  (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
  (φ : M.C.functionField →+* M'.C.functionField)
  (hφk : ∀ a : k, φ (baseToFunctionField M.toBase a) = baseToFunctionField M'.toBase a)
  (hφnat : ∀ (p : M'.C) (s : M.C.presheaf.stalk (π.base p)),
    algebraMap _ M'.C.functionField (π.stalkMap p s) = φ (algebraMap _ M.C.functionField s))
include hπ hφk hφnat in
omit [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F'] in
Lean source · statement
theorem vanishesAt_psi_sub
    (hplace : ∀ (y : {q : Spec (CommRingCat.of k) ⟶ M'.C // q ≫ M'.toBase = 𝟙 _})
        (x : {q : Spec (CommRingCat.of k) ⟶ M.C // q ≫ M.toBase = 𝟙 _}),
      y.1 ≫ π = x.1 → (M'.pointEquivPlace y).restrict F = M.pointEquivPlace x)
    (y : {q : Spec (CommRingCat.of k) ⟶ M'.C // q ≫ M'.toBase = 𝟙 _})
    (s : M.C.presheaf.stalk (π.base (pointEquivClosedPoint M'.toBase y).1)) :
    VanishesAt (M'.pointEquivPlace y)
      (psi M M' φ (stalkToField M _ s) - algebraMap F F' (stalkToField M _ s))
theorem

key

L378 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRigidity.key
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
namespace HG1bRigidity
open IsLocalRing AlgebraicCurve
section Rigidity
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v
variable {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F']
  [Algebra k F] [Algebra k F']
  [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
  [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
  (M : CurveModel k F) (M' : CurveModel k F')
  (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
  (φ : M.C.functionField →+* M'.C.functionField)
  (hφk : ∀ a : k, φ (baseToFunctionField M.toBase a) = baseToFunctionField M'.toBase a)
  (hφnat : ∀ (p : M'.C) (s : M.C.presheaf.stalk (π.base p)),
    algebraMap _ M'.C.functionField (π.stalkMap p s) = φ (algebraMap _ M.C.functionField s))
include hπ hφk hφnat in
omit [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F'] in
Lean source · statement
theorem key
    (hplace : ∀ (y : {q : Spec (CommRingCat.of k) ⟶ M'.C // q ≫ M'.toBase = 𝟙 _})
        (x : {q : Spec (CommRingCat.of k) ⟶ M.C // q ≫ M.toBase = 𝟙 _}),
      y.1 ≫ π = x.1 → (M'.pointEquivPlace y).restrict F = M.pointEquivPlace x)
    (f : F) : M'.ffEquiv.symm (φ (M.ffEquiv f)) = algebraMap F F' f
theorem

apply_genericPoint_eq

L442 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRig.apply_genericPoint_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
section RigiditySchemeSide
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve Topology
universe u v
namespace HG1bRig
variable {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F'] [Algebra k F]
  [Algebra k F']
    [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
    [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
    (M : CurveModel k F) (M' : CurveModel k F')
    (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
    [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
omit [IsAlgClosed k] [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F]
  [Algebra.EssFiniteType k F']
  [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] [IsFinite π]
    [LocallyOfFinitePresentation π] in
Lean source · statement
theorem apply_genericPoint_eq : π.base (genericPoint M'.C) = genericPoint M.C
def

fieldMap

L454 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRig.fieldMap
Documentation

The function-field homomorphism induced by the morphism of curve models.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
section RigiditySchemeSide
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve Topology
universe u v
namespace HG1bRig
variable {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F'] [Algebra k F]
  [Algebra k F']
    [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
    [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
    (M : CurveModel k F) (M' : CurveModel k F')
    (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
    [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
Lean source · statement
def fieldMap : M.C.functionField →+* M'.C.functionField
theorem

algebraMap_stalkMap

L462 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRig.algebraMap_stalkMap
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
section RigiditySchemeSide
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve Topology
universe u v
namespace HG1bRig
variable {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F'] [Algebra k F]
  [Algebra k F']
    [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
    [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
    (M : CurveModel k F) (M' : CurveModel k F')
    (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
    [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
omit [IsAlgClosed k] [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F]
  [Algebra.EssFiniteType k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
    [IsFinite π] [LocallyOfFinitePresentation π] in
Lean source · statement
theorem algebraMap_stalkMap (p : M'.C) (s : M.C.presheaf.stalk (π.base p)) :
    algebraMap _ M'.C.functionField (π.stalkMap p s) = fieldMap M M' π (algebraMap _
      M.C.functionField s)
theorem

fieldMap_baseToFunctionField

L476 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRig.fieldMap_baseToFunctionField
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
section RigiditySchemeSide
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve Topology
universe u v
namespace HG1bRig
variable {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F'] [Algebra k F]
  [Algebra k F']
    [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
    [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
    (M : CurveModel k F) (M' : CurveModel k F')
    (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
    [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
include hπ in
omit [IsAlgClosed k] [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F]
  [Algebra.EssFiniteType k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
    [IsFinite π] [LocallyOfFinitePresentation π] in
Lean source · statement
theorem fieldMap_baseToFunctionField (a : k) :
    fieldMap M M' π (baseToFunctionField M.toBase a) = baseToFunctionField M'.toBase a
theorem

rigidity_of_key

L494 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap.HG1bRig.rigidity_of_key
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
section RigiditySchemeSide
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve Topology
universe u v
namespace HG1bRig
variable {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F'] [Algebra k F]
  [Algebra k F']
    [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
    [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
    (M : CurveModel k F) (M' : CurveModel k F')
    (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
    [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
include hπ in
omit [IsAlgClosed k] [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F]
  [Algebra.EssFiniteType k F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] [IsFinite π]
    [LocallyOfFinitePresentation π] in
Lean source · statement
theorem rigidity_of_key
    (key : ∀ (φ : M.C.functionField →+* M'.C.functionField)
      (_hφk : ∀ a : k, φ (baseToFunctionField M.toBase a) = baseToFunctionField M'.toBase a)
      (_hφnat : ∀ (p : M'.C) (s : M.C.presheaf.stalk (π.base p)),
        algebraMap _ M'.C.functionField (π.stalkMap p s) = φ (algebraMap _ M.C.functionField s))
      (f : F), M'.ffEquiv.symm (φ (M.ffEquiv f)) = algebraMap F F' f)
    (p : M'.C) (s : M.C.presheaf.stalk (π.base p)) :
    M'.ffEquiv.symm (algebraMap _ M'.C.functionField (π.stalkMap p s)) =
      algebraMap F F' (M.ffEquiv.symm (algebraMap _ M.C.functionField s))
theorem

ffEquiv_symm_stalkMap_eq_algebraMap

L517 ↗
AlgebraicCurve.CurveModel.ffEquiv_symm_stalkMap_eq_algebraMap
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ffEquiv_symm_stalkMap_eq_algebraMap
section RigiditySolution
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
universe u v
Lean source · statement
theorem _root_.AlgebraicCurve.CurveModel.ffEquiv_symm_stalkMap_eq_algebraMap
    {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F'] [Algebra k F]
      [Algebra k F']
    [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
    [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
    (M : CurveModel k F) (M' : CurveModel k F')
    (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
    [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
    (hplace : ∀ (y : {q : Spec (CommRingCat.of k) ⟶ M'.C // q ≫ M'.toBase = 𝟙 _})
        (x : {q : Spec (CommRingCat.of k) ⟶ M.C // q ≫ M.toBase = 𝟙 _}),
      y.1 ≫ π = x.1 → (M'.pointEquivPlace y).restrict F = M.pointEquivPlace x)
    (p : M'.C) (s : M.C.presheaf.stalk (π.base p)) :
    M'.ffEquiv.symm (algebraMap _ M'.C.functionField (π.stalkMap p s)) =
      algebraMap F F' (M.ffEquiv.symm (algebraMap _ M.C.functionField s))

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