NYLL
Module

CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint.lean

Nyll.AlgebraicCurves.Models.CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint
6 declarations indexed from sourceView source ↗

Module documentation

Curve Model sub algebra Map mem of has Value place Of Point

Imports2
Imported by1

Declarations

theorem

algebraMap_stalk_injective

L42 ↗
AlgebraicCurves.Models.Proofs.CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint.AlgebraicCurve.CurveModel.PlaceRead.algebraMap_stalk_injective
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace PlaceRead
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
Lean source · statement
theorem algebraMap_stalk_injective {X : Scheme.{u}} [IsIntegral X] (x : X) :
    Function.Injective (algebraMap (X.presheaf.stalk x) X.functionField)
theorem

not_isUnit_germ_appIso_inv_of_mem

L56 ↗
AlgebraicCurves.Models.Proofs.CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint.AlgebraicCurve.CurveModel.PlaceRead.not_isUnit_germ_appIso_inv_of_mem
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace PlaceRead
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
Lean source · statement
theorem not_isUnit_germ_appIso_inv_of_mem {X : Scheme.{u}} {B : CommRingCat.{u}} (G : Spec B ⟶ X)
  [IsOpenImmersion G]
    (z : ↥(Spec B)) (f : B) (hf : f ∈ z.asIdeal) :
    ¬ IsUnit (X.presheaf.germ (G ''ᵁ ⊤) (G.base z) ⟨z, trivial, rfl⟩ ((G.appIso ⊤).inv
      ((Scheme.ΓSpecIso B).inv f)))
theorem

germToFunctionField_appIso_inv_base

L70 ↗
AlgebraicCurves.Models.Proofs.CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint.AlgebraicCurve.CurveModel.PlaceRead.germToFunctionField_appIso_inv_base
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace PlaceRead
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
Lean source · statement
theorem germToFunctionField_appIso_inv_base {Y : Scheme.{u}} [IsIntegral Y] {B : CommRingCat.{u}}
  (G : Spec B ⟶ Y)
    [IsOpenImmersion G] {K : Type u} [Field K] (y : Y ⟶ Spec (CommRingCat.of K)) (c :
      CommRingCat.of K ⟶ B)
    (hc : G ≫ y = Spec.map c) [Nonempty ((G ''ᵁ ⊤ : Y.Opens) : Scheme.{u})] (k : K) :
    Y.germToFunctionField (G ''ᵁ ⊤) ((G.appIso ⊤).inv ((Scheme.ΓSpecIso B).inv (c k))) =
      baseToFunctionField y k
theorem

hasValue_placeOfPoint_of_sub_algebraMap_mem

L89 ↗
AlgebraicCurves.Models.Proofs.CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint.AlgebraicCurve.CurveModel.PlaceRead.hasValue_placeOfPoint_of_sub_algebraMap_mem
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace PlaceRead
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
theorem hasValue_placeOfPoint_of_sub_algebraMap_mem (M : CurveModel K L)
    {B : Type u} [CommRing B] [Algebra K B] (G : Spec (CommRingCat.of B) ⟶ M.C) [IsOpenImmersion G]
    (hG : G ≫ M.toBase = Spec.map (CommRingCat.ofHom (algebraMap K B)))
    [Nonempty ((G ''ᵁ ⊤ : M.C.Opens) : Scheme.{u})]
    (z : ↥(Spec (CommRingCat.of B))) (hz : G.base z ∈ closedPoints M.C)
    (f : B) (a : K) (hfa : f - algebraMap K B a ∈ z.asIdeal) :
    (M.placeOfPoint ⟨G.base z, hz⟩).HasValue
      (M.ffEquiv.symm (M.C.germToFunctionField (G ''ᵁ ⊤)
        ((G.appIso ⊤).inv ((Scheme.ΓSpecIso (CommRingCat.of B)).inv f)))) a
theorem

sub_algebraMap_mem_of_hasValue_placeOfPoint

L152 ↗
AlgebraicCurves.Models.Proofs.CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint.AlgebraicCurve.CurveModel.PlaceRead.sub_algebraMap_mem_of_hasValue_placeOfPoint
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CurveModel
open _root_.AlgebraicCurve.CurveModel
namespace PlaceRead
open _root_.AlgebraicCurve.CurveModel
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
theorem sub_algebraMap_mem_of_hasValue_placeOfPoint (M : CurveModel K L)
    {B : Type u} [CommRing B] [Algebra K B] (G : Spec (CommRingCat.of B) ⟶ M.C) [IsOpenImmersion G]
    (hG : G ≫ M.toBase = Spec.map (CommRingCat.ofHom (algebraMap K B)))
    [Nonempty ((G ''ᵁ ⊤ : M.C.Opens) : Scheme.{u})]
    (z : ↥(Spec (CommRingCat.of B))) (hz : G.base z ∈ closedPoints M.C)
    (f : B) (a : K)
    (hv : (M.placeOfPoint ⟨G.base z, hz⟩).HasValue
      (M.ffEquiv.symm (M.C.germToFunctionField (G ''ᵁ ⊤)
        ((G.appIso ⊤).inv ((Scheme.ΓSpecIso (CommRingCat.of B)).inv f)))) a) :
    f - algebraMap K B a ∈ z.asIdeal
theorem

sub_algebraMap_mem_of_hasValue_placeOfPoint

L217 ↗
AlgebraicCurve.CurveModel.sub_algebraMap_mem_of_hasValue_placeOfPoint
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_sub_algebraMap_mem_of_hasValue_placeOfPoint
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v
noncomputable section
Lean source · statement
theorem _root_.AlgebraicCurve.CurveModel.sub_algebraMap_mem_of_hasValue_placeOfPoint
    {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (M : CurveModel K L)
    {B : Type u} [CommRing B] [Algebra K B] (G : Spec (CommRingCat.of B) ⟶ M.C) [IsOpenImmersion G]
    (hG : G ≫ M.toBase = Spec.map (CommRingCat.ofHom (algebraMap K B)))
    [Nonempty (Scheme.Opens.toScheme (G ''ᵁ ⊤))]
    (z : ↥(Spec (CommRingCat.of B))) (hz : G.base z ∈ closedPoints M.C)
    (f : B) (a : K)
    (hv : (M.placeOfPoint ⟨G.base z, hz⟩).HasValue
      (M.ffEquiv.symm (M.C.germToFunctionField (G ''ᵁ ⊤)
        ((G.appIso ⊤).inv ((Scheme.ΓSpecIso (CommRingCat.of B)).inv f)))) a) :
    f - algebraMap K B a ∈ z.asIdeal

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