NYLL
Module

Transport.lean

Nyll.AlgebraicCurves.Models.Transport
31 declarations indexed from sourceView source ↗

Module documentation

Transport

Imports1
Imported by2

Declarations

theorem

inv_base_genericPoint

L31 ↗
AlgebraicCurve.inv_base_genericPoint
Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
theorem inv_base_genericPoint (e : X ≅ Y) : e.inv.base (genericPoint Y) = genericPoint X
theorem

hom_base_genericPoint

L34 ↗
AlgebraicCurve.hom_base_genericPoint
Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
theorem hom_base_genericPoint (e : X ≅ Y) : e.hom.base (genericPoint X) = genericPoint Y
def

functionFieldHomOfIso

L38 ↗
AlgebraicCurve.functionFieldHomOfIso
Documentation

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

Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
def functionFieldHomOfIso (e : X ≅ Y) : X.functionField ⟶ Y.functionField
theorem

isIso_stalkSpecializes_of_eq

L42 ↗
AlgebraicCurve.isIso_stalkSpecializes_of_eq
Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
theorem isIso_stalkSpecializes_of_eq {Z : Scheme.{u}} {x y : Z} (h : x = y) :
    IsIso (Z.presheaf.stalkSpecializes (specializes_of_eq h))
instance

isIso_functionFieldHomOfIso

L48 ↗
AlgebraicCurve.isIso_functionFieldHomOfIso
Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
instance isIso_functionFieldHomOfIso (e : X ≅ Y) : IsIso (functionFieldHomOfIso e)
def

functionFieldIsoOfIso

L53 ↗
AlgebraicCurve.functionFieldIsoOfIso
Documentation

The ring equivalence of function fields induced by an isomorphism of integral schemes.

Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
def functionFieldIsoOfIso (e : X ≅ Y) : X.functionField ≃+* Y.functionField
theorem

functionFieldIsoOfIso_apply

L56 ↗
AlgebraicCurve.functionFieldIsoOfIso_apply
Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
theorem functionFieldIsoOfIso_apply (e : X ≅ Y) (z : X.functionField) :
    functionFieldIsoOfIso e z = (functionFieldHomOfIso e).hom z
theorem

ofHom_functionFieldIsoOfIso

L59 ↗
AlgebraicCurve.ofHom_functionFieldIsoOfIso
Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
theorem ofHom_functionFieldIsoOfIso (e : X ≅ Y) :
    CommRingCat.ofHom (functionFieldIsoOfIso e).toRingHom = functionFieldHomOfIso e
theorem

fromSpecStalk_comp_inv_eq_specMap_functionFieldIsoOfIso

L63 ↗
AlgebraicCurve.fromSpecStalk_comp_inv_eq_specMap_functionFieldIsoOfIso
Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
theorem fromSpecStalk_comp_inv_eq_specMap_functionFieldIsoOfIso (e : X ≅ Y) :
    Y.fromSpecStalk (genericPoint Y) ≫ e.inv =
      Spec.map (CommRingCat.ofHom (functionFieldIsoOfIso e).toRingHom) ≫ X.fromSpecStalk
        (genericPoint X)
theorem

fromSpecStalk_eq_specMap_functionFieldIsoOfIso_comp_hom

L70 ↗
AlgebraicCurve.fromSpecStalk_eq_specMap_functionFieldIsoOfIso_comp_hom
Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
theorem fromSpecStalk_eq_specMap_functionFieldIsoOfIso_comp_hom (e : X ≅ Y) :
    Y.fromSpecStalk (genericPoint Y) =
      Spec.map (CommRingCat.ofHom (functionFieldIsoOfIso e).toRingHom) ≫ X.fromSpecStalk
        (genericPoint X) ≫ e.hom
theorem

germ_comp_functionFieldHomOfIso

L78 ↗
AlgebraicCurve.germ_comp_functionFieldHomOfIso
Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
theorem germ_comp_functionFieldHomOfIso (e : X ≅ Y) :
    X.presheaf.germ (⊤ : X.Opens) (genericPoint X) (Set.mem_univ _) ≫ functionFieldHomOfIso e =
      e.inv.appTop ≫ Y.presheaf.germ (⊤ : Y.Opens) (genericPoint Y) (Set.mem_univ _)
theorem

stalkToFunctionField_comp_functionFieldHomOfIso

L84 ↗
AlgebraicCurve.stalkToFunctionField_comp_functionFieldHomOfIso
Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
theorem stalkToFunctionField_comp_functionFieldHomOfIso (e : X ≅ Y) (y : Y) :
    X.presheaf.stalkSpecializes ((genericPoint_spec X).specializes (Set.mem_univ (e.inv.base y))) ≫
        functionFieldHomOfIso e =
      e.inv.stalkMap y ≫ Y.presheaf.stalkSpecializes ((genericPoint_spec Y).specializes
        (Set.mem_univ y))
theorem

functionFieldIsoOfIso_algebraMap_stalk

L93 ↗
AlgebraicCurve.functionFieldIsoOfIso_algebraMap_stalk
Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
theorem functionFieldIsoOfIso_algebraMap_stalk (e : X ≅ Y) (y : Y) (s : X.presheaf.stalk
  (e.inv.base y)) :
    functionFieldIsoOfIso e (algebraMap (X.presheaf.stalk (e.inv.base y)) X.functionField s) =
      algebraMap (Y.presheaf.stalk y) Y.functionField (e.inv.stalkMap y s)
theorem

functionFieldIsoOfIso_baseToFunctionField

L102 ↗
AlgebraicCurve.functionFieldIsoOfIso_baseToFunctionField
Source context 6 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
section FunctionFieldIso
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
Lean source · statement
theorem functionFieldIsoOfIso_baseToFunctionField {K : Type u} [Field K]
    (cX : X ⟶ Spec (CommRingCat.of K)) (cY : Y ⟶ Spec (CommRingCat.of K)) (e : X ≅ Y) (he : e.hom ≫
      cY = cX) (a : K) :
    functionFieldIsoOfIso e (baseToFunctionField cX a) = baseToFunctionField cY a
theorem

mem_closedPoints_of_iso

L128 ↗
AlgebraicCurve.CurveModel.mem_closedPoints_of_iso
Source context 8 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section ClosedPoints
variable {X Y : Scheme.{u}}
Lean source · statement
theorem mem_closedPoints_of_iso {Z W : Scheme.{u}} (f : Z ⟶ W) [IsIso f] {z : Z} (hz : z ∈
  closedPoints Z) :
    f.base z ∈ closedPoints W
def

closedPointsEquivOfIso

L135 ↗
AlgebraicCurve.CurveModel.closedPointsEquivOfIso
Documentation

The equivalence of closed points induced contravariantly by a scheme isomorphism.

Source context 8 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section ClosedPoints
variable {X Y : Scheme.{u}}
Lean source · full declaration
def closedPointsEquivOfIso (e : X ≅ Y) : closedPoints Y ≃ closedPoints X where
  toFun y := ⟨e.inv.base y.1, mem_closedPoints_of_iso e.inv y.2⟩
  invFun x := ⟨e.hom.base x.1, mem_closedPoints_of_iso e.hom x.2⟩
  left_inv y := Subtype.ext (by
    change (e.inv ≫ e.hom).base y.1 = y.1
    rw [e.inv_hom_id]; rfl)
  right_inv x := Subtype.ext (by
    change (e.hom ≫ e.inv).base x.1 = x.1
    rw [e.hom_inv_id]; rfl)
theorem

closedPointsEquivOfIso_apply_coe

L145 ↗
AlgebraicCurve.CurveModel.closedPointsEquivOfIso_apply_coe
Source context 8 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section ClosedPoints
variable {X Y : Scheme.{u}}
Lean source · statement
theorem closedPointsEquivOfIso_apply_coe (e : X ≅ Y) (y : closedPoints Y) :
    ((closedPointsEquivOfIso e y : closedPoints X) : X) = e.inv.base y.1
theorem

toBase_eq

L156 ↗
AlgebraicCurve.CurveModel.toBase_eq
Source context 9 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
include he in
Lean source · statement
theorem toBase_eq : c = e.inv ≫ Mdl.toBase
theorem

isIntegral_of_iso

L158 ↗
AlgebraicCurve.CurveModel.isIntegral_of_iso
Source context 9 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
include Mdl e in
Lean source · statement
theorem isIntegral_of_iso : IsIntegral C
theorem

isProper_of_iso

L160 ↗
AlgebraicCurve.CurveModel.isProper_of_iso
Source context 9 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
include he in
Lean source · statement
theorem isProper_of_iso : IsProper c
theorem

smooth_of_iso

L163 ↗
AlgebraicCurve.CurveModel.smooth_of_iso
Source context 9 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
include he in
Lean source · statement
theorem smooth_of_iso : SmoothOfRelativeDimension 1 c
theorem

range_stalk_eq_of_iso

L167 ↗
AlgebraicCurve.CurveModel.range_stalk_eq_of_iso
Source context 8 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
Lean source · full declaration
theorem range_stalk_eq_of_iso (x : closedPoints C) :
    letI := isIntegral_of_iso Mdl e
    (((Mdl.ffEquiv.trans (functionFieldIsoOfIso e)).symm : C.functionField ≃+* L).toRingHom.comp
        (algebraMap (C.presheaf.stalk x.1) C.functionField)).range =
      (Mdl.placeOfPoint (closedPointsEquivOfIso e x)).toValuationSubring.toSubring := by
  let := isIntegral_of_iso Mdl e
  rw [← Mdl.range_stalk_eq (closedPointsEquivOfIso e x)]
  change _ = ((Mdl.ffEquiv.symm : Mdl.C.functionField ≃+* L).toRingHom.comp
    (algebraMap (Mdl.C.presheaf.stalk (e.inv.base x.1)) Mdl.C.functionField)).range
  have hsurj : Function.Surjective (e.inv.stalkMap x.1).hom :=
    (asIso (e.inv.stalkMap x.1)).commRingCatIsoToRingEquiv.surjective
  ext z
  simp only [RingHom.mem_range, RingHom.coe_comp, Function.comp_apply, RingEquiv.toRingHom_eq_coe,
    RingEquiv.coe_toRingHom]
  constructor
  · rintro ⟨t, rfl⟩
    obtain ⟨s, rfl⟩ := hsurj t
    refine ⟨s, ?_⟩
    rw [RingEquiv.symm_trans_apply, ← functionFieldIsoOfIso_algebraMap_stalk,
      RingEquiv.symm_apply_apply]
  · rintro ⟨s, rfl⟩
    refine ⟨(e.inv.stalkMap x.1).hom s, ?_⟩
    rw [RingEquiv.symm_trans_apply, ← functionFieldIsoOfIso_algebraMap_stalk,
      RingEquiv.symm_apply_apply]
def

transport

L193 ↗
AlgebraicCurve.CurveModel.transport
Documentation

Transport of a curve model along a compatible scheme isomorphism.

Source context 8 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
Lean source · statement
def transport : CurveModel K L
theorem

transport_C

L213 ↗
AlgebraicCurve.CurveModel.transport_C
Source context 8 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
Lean source · statement
theorem transport_C : (Mdl.transport c e he).C = C
theorem

transport_toBase

L215 ↗
AlgebraicCurve.CurveModel.transport_toBase
Source context 8 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
Lean source · statement
theorem transport_toBase : (Mdl.transport c e he).toBase = c
theorem

transport_ffEquiv

L217 ↗
AlgebraicCurve.CurveModel.transport_ffEquiv
Source context 8 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
Lean source · full declaration
theorem transport_ffEquiv :
    (Mdl.transport c e he).ffEquiv =
      (letI := isIntegral_of_iso Mdl e; Mdl.ffEquiv.trans (functionFieldIsoOfIso e)) := rfl
theorem

transport_ffEquiv_apply

L221 ↗
AlgebraicCurve.CurveModel.transport_ffEquiv_apply
Source context 8 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
Lean source · full declaration
theorem transport_ffEquiv_apply (f : L) :
    (Mdl.transport c e he).ffEquiv f = (letI := isIntegral_of_iso Mdl e; functionFieldIsoOfIso e
      (Mdl.ffEquiv f)) := rfl
theorem

transport_ffEquiv_symm_apply

L225 ↗
AlgebraicCurve.CurveModel.transport_ffEquiv_symm_apply
Source context 8 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
Lean source · full declaration
theorem transport_ffEquiv_symm_apply (z : (Mdl.transport c e he).C.functionField) :
    (Mdl.transport c e he).ffEquiv.symm z =
      (letI := isIntegral_of_iso Mdl e; Mdl.ffEquiv.symm ((functionFieldIsoOfIso e).symm z)) := rfl
theorem

transport_placeOfPoint

L229 ↗
AlgebraicCurve.CurveModel.transport_placeOfPoint
Source context 8 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
Lean source · statement
theorem transport_placeOfPoint (x : closedPoints C) :
    (Mdl.transport c e he).placeOfPoint x = Mdl.placeOfPoint (closedPointsEquivOfIso e x)
theorem

transport_placeOfPoint'

L232 ↗
AlgebraicCurve.CurveModel.transport_placeOfPoint'
Source context 8 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
Lean source · statement
theorem transport_placeOfPoint' (x : closedPoints C) :
    (Mdl.transport c e he).placeOfPoint x =
      Mdl.placeOfPoint ⟨e.inv.base x.1, (closedPointsEquivOfIso e x).2⟩
theorem

transport_pointEquivPlace

L236 ↗
AlgebraicCurve.CurveModel.transport_pointEquivPlace
Source context 8 commands

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

universe u v
open CategoryTheory AlgebraicGeometry
noncomputable section
namespace AlgebraicCurve
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
section Transport
variable (Mdl : CurveModel K L) {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K)) (e : Mdl.C ≅ C)
  (he : e.hom ≫ c = Mdl.toBase)
Lean source · full declaration
theorem transport_pointEquivPlace [IsAlgClosed K]
    (x : {q : Spec (CommRingCat.of K) ⟶ C // q ≫ c = 𝟙 _}) :
    (Mdl.transport c e he).pointEquivPlace x =
      Mdl.pointEquivPlace ⟨x.1 ≫ e.inv, by rw [Category.assoc, ← toBase_eq Mdl c e he, x.2]⟩ := by
  let : SmoothOfRelativeDimension 1 c := (Mdl.transport c e he).smooth
  let : Smooth c := SmoothOfRelativeDimension.smooth 1 c
  change Mdl.placeOfPoint (closedPointsEquivOfIso e (pointEquivClosedPoint c x)) =
    Mdl.placeOfPoint (pointEquivClosedPoint Mdl.toBase
      ⟨x.1 ≫ e.inv, by rw [Category.assoc, ← toBase_eq Mdl c e he, x.2]⟩)
  congr 1

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