structure ArithmeticGeometry.Thm19_2.FunctionFieldCat (k : Type u) [Field k] : Type (u + 1)

• carrier : Type u
• fieldInst : Field self.carrier
• algInst : Algebra k self.carrier
• finitelyGenerated : ⊤.FG
• transcendenceDegreeOne : ∃ (x : self.carrier), Transcendental k x ∧ Algebra.IsAlgebraic (↥k⟮x⟯) self.carrier
• algClosedInF (x : self.carrier) : IsAlgebraic k x → x ∈ Set.range ⇑(algebraMap k self.carrier)

@[implicit_reducible]

instance ArithmeticGeometry.Thm19_2.instCoeSortFunctionFieldCatType (k : Type u) [Field k] : CoeSort (FunctionFieldCat k) (Type u)

structure ArithmeticGeometry.Thm19_2.FunctionFieldCat.Hom (k : Type u) [Field k] (F₁ F₂ : FunctionFieldCat k) : Type u

• toAlgHom : F₁.carrier →ₐ[k] F₂.carrier

theorem ArithmeticGeometry.Thm19_2.FunctionFieldCat.Hom.ext_iff {k : Type u} {inst✝ : Field k} {F₁ F₂ : FunctionFieldCat k} {x y : Hom k F₁ F₂} : x = y ↔ x.toAlgHom = y.toAlgHom

theorem ArithmeticGeometry.Thm19_2.FunctionFieldCat.Hom.ext {k : Type u} {inst✝ : Field k} {F₁ F₂ : FunctionFieldCat k} {x y : Hom k F₁ F₂} (toAlgHom : x.toAlgHom = y.toAlgHom) : x = y

@[implicit_reducible]

instance ArithmeticGeometry.Thm19_2.instCategoryFunctionFieldCat (k : Type u) [Field k] : CategoryTheory.Category.{u, u + 1} (FunctionFieldCat k)

structure ArithmeticGeometry.Thm19_2.SmProjCurve (k : Type u) [Field k] : Type (u + 1)

• toScheme : AlgebraicGeometry.Scheme
• structureMorphism : self.toScheme ⟶ AlgebraicGeometry.Spec (CommRingCat.of k)
• isIntegral : AlgebraicGeometry.IsIntegral self.toScheme
• isProper : AlgebraicGeometry.IsProper self.structureMorphism
• isSmooth : AlgebraicGeometry.SmoothOfRelativeDimension 1 self.structureMorphism

structure ArithmeticGeometry.Thm19_2.SmProjCurve.Hom (k : Type u) [Field k] (C₁ C₂ : SmProjCurve k) : Type u

• toSchemeHom : C₁.toScheme ⟶ C₂.toScheme
• over_spec : CategoryTheory.CategoryStruct.comp self.toSchemeHom C₂.structureMorphism = C₁.structureMorphism

theorem ArithmeticGeometry.Thm19_2.SmProjCurve.Hom.ext_iff {k : Type u} {inst✝ : Field k} {C₁ C₂ : SmProjCurve k} {x y : Hom k C₁ C₂} : x = y ↔ x.toSchemeHom = y.toSchemeHom

theorem ArithmeticGeometry.Thm19_2.SmProjCurve.Hom.ext {k : Type u} {inst✝ : Field k} {C₁ C₂ : SmProjCurve k} {x y : Hom k C₁ C₂} (toSchemeHom : x.toSchemeHom = y.toSchemeHom) : x = y

@[implicit_reducible]

instance ArithmeticGeometry.Thm19_2.SmProjCurve.categoryInstance (k : Type u) [Field k] : CategoryTheory.Category.{u, u + 1} (SmProjCurve k)

noncomputable def ArithmeticGeometry.Thm19_2.SmProjCurve.algebraMapHom (k : Type u) [Field k] (C : SmProjCurve k) : CommRingCat.of k ⟶ C.toScheme.functionField

@[implicit_reducible]

noncomputable instance ArithmeticGeometry.Thm19_2.SmProjCurve.algebraFunctionField (k : Type u) [Field k] (C : SmProjCurve k) : Algebra k ↑C.toScheme.functionField

theorem ArithmeticGeometry.Thm19_2.SmProjCurve.funField_finitelyGenerated (k : Type u) [Field k] [PerfectField k] (C : SmProjCurve k) : ⊤.FG

theorem ArithmeticGeometry.Thm19_2.SmProjCurve.funField_transcendenceDegreeOne (k : Type u) [Field k] [PerfectField k] (C : SmProjCurve k) : ∃ (x : ↑C.toScheme.functionField), Transcendental k x ∧ Algebra.IsAlgebraic ↥k⟮x⟯ ↑C.toScheme.functionField

theorem ArithmeticGeometry.Thm19_2.SmProjCurve.funField_algClosedInF (k : Type u) [Field k] [PerfectField k] (C : SmProjCurve k) (x : ↑C.toScheme.functionField) : IsAlgebraic k x → x ∈ Set.range ⇑(algebraMap k ↑C.toScheme.functionField)

noncomputable def ArithmeticGeometry.Thm19_2.SmProjCurve.toFunctionFieldCat (k : Type u) [Field k] [PerfectField k] (C : SmProjCurve k) : FunctionFieldCat k

theorem ArithmeticGeometry.Thm19_2.SmProjCurve.Hom.map_genericPoint (k : Type u) [Field k] [PerfectField k] {C₁ C₂ : SmProjCurve k} (f : C₁ ⟶ C₂) : f.toSchemeHom (genericPoint ↥C₁.toScheme) = genericPoint ↥C₂.toScheme

theorem ArithmeticGeometry.Thm19_2.SmProjCurve.Hom.pullback_algebraMap_commutes (k : Type u) [Field k] [PerfectField k] {C₁ C₂ : SmProjCurve k} (f : C₁ ⟶ C₂) (r : k) : have x := ⋯; have x_1 := ⋯; (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (C₂.toScheme.presheaf.stalkCongr ⋯).hom (AlgebraicGeometry.Scheme.Hom.stalkMap f.toSchemeHom (genericPoint ↥C₁.toScheme)))) ((algebraMap k (toFunctionFieldCat k C₂).carrier) r) = (algebraMap k (toFunctionFieldCat k C₁).carrier) r

noncomputable def ArithmeticGeometry.Thm19_2.SmProjCurve.Hom.pullbackAlgHom (k : Type u) [Field k] [PerfectField k] {C₁ C₂ : SmProjCurve k} (f : C₁ ⟶ C₂) : toFunctionFieldCat k C₂ ⟶ toFunctionFieldCat k C₁

theorem ArithmeticGeometry.Thm19_2.SmProjCurve.Hom.pullbackAlgHom_id (k : Type u) [Field k] [PerfectField k] (C : SmProjCurve k) : pullbackAlgHom k (CategoryTheory.CategoryStruct.id C) = CategoryTheory.CategoryStruct.id (toFunctionFieldCat k C)

theorem ArithmeticGeometry.Thm19_2.SmProjCurve.Hom.pullbackAlgHom_comp (k : Type u) [Field k] [PerfectField k] {C₁ C₂ C₃ : SmProjCurve k} (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) : pullbackAlgHom k (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (pullbackAlgHom k g) (pullbackAlgHom k f)

noncomputable def ArithmeticGeometry.Thm19_2.functionFieldFunctor (k : Type u) [Field k] [PerfectField k] : CategoryTheory.Functor (SmProjCurve k)ᵒᵖ (FunctionFieldCat k)

theorem ArithmeticGeometry.Thm19_2.SmProjCurve.fromSpecStalk_genericPoint_isDominant (k : Type u) [Field k] [PerfectField k] (C : SmProjCurve k) : AlgebraicGeometry.IsDominant (C.toScheme.fromSpecStalk (genericPoint ↥C.toScheme))

theorem ArithmeticGeometry.Thm19_2.SmProjCurve.Hom.ext_of_fromSpecStalk_genericPoint (k : Type u) [Field k] [PerfectField k] {C₁ C₂ : SmProjCurve k} (f g : C₁ ⟶ C₂) (h : CategoryTheory.CategoryStruct.comp (C₁.toScheme.fromSpecStalk (genericPoint ↥C₁.toScheme)) f.toSchemeHom = CategoryTheory.CategoryStruct.comp (C₁.toScheme.fromSpecStalk (genericPoint ↥C₁.toScheme)) g.toSchemeHom) : f = g

theorem ArithmeticGeometry.Thm19_2.SmProjCurve.Hom.pullbackAlgHom_eq_imp_fromSpecStalk_eq (k : Type u) [Field k] [PerfectField k] {C₁ C₂ : SmProjCurve k} (f g : C₁ ⟶ C₂) (h : pullbackAlgHom k f = pullbackAlgHom k g) : CategoryTheory.CategoryStruct.comp (C₁.toScheme.fromSpecStalk (genericPoint ↥C₁.toScheme)) f.toSchemeHom = CategoryTheory.CategoryStruct.comp (C₁.toScheme.fromSpecStalk (genericPoint ↥C₁.toScheme)) g.toSchemeHom

theorem ArithmeticGeometry.Thm19_2.functionFieldFunctor_faithful (k : Type u) [Field k] [PerfectField k] : (functionFieldFunctor k).Faithful

instance ArithmeticGeometry.Thm19_2.FunctionFieldCat.toFunctionField_k (k : Type u) [Field k] (F : FunctionFieldCat k) : FunctionField_k k F.carrier

theorem ArithmeticGeometry.Thm19_2.SmoothProjectiveCurveData_realizes_as_SmProjCurve {k : Type u} [Field k] [PerfectField k] (F : FunctionFieldCat k) {n : ℕ} (C : SmoothProjectiveCurveData k F.carrier n) : ∃ (S : SmProjCurve k), Nonempty (SmProjCurve.toFunctionFieldCat k S ≅ F)

theorem ArithmeticGeometry.Thm19_2.smoothProjectiveModel (k : Type u) [Field k] [PerfectField k] (F : FunctionFieldCat k) : ∃ (C : SmProjCurve k), Nonempty (SmProjCurve.toFunctionFieldCat k C ≅ F)

theorem ArithmeticGeometry.Thm19_2.dvr_surjective_algHom_lifts_to_schemeMorphism {k : Type u} [Field k] [PerfectField k] {C₁ C₂ : SmProjCurve k} (θ : SmProjCurve.toFunctionFieldCat k C₂ ⟶ SmProjCurve.toFunctionFieldCat k C₁) (hSurj : ∀ (P : DVROfFunctionField k (SmProjCurve.toFunctionFieldCat k C₁).carrier), ∃ (Q : DVROfFunctionField k (SmProjCurve.toFunctionFieldCat k C₂).carrier), ∀ f ∈ Q.valRing, θ.toAlgHom f ∈ P.valRing) : ∃ (f : C₁ ⟶ C₂), SmProjCurve.Hom.pullbackAlgHom k f = θ

theorem ArithmeticGeometry.Thm19_2.morphism_constant_or_surjective_fullness_witness {k : Type u} [Field k] [PerfectField k] {C₁ C₂ : SmProjCurve k} (θ : SmProjCurve.toFunctionFieldCat k C₂ ⟶ SmProjCurve.toFunctionFieldCat k C₁) (P : DVROfFunctionField k (SmProjCurve.toFunctionFieldCat k C₁).carrier) : ∃ (Q : DVROfFunctionField k (SmProjCurve.toFunctionFieldCat k C₂).carrier), ∀ f ∈ Q.valRing, θ.toAlgHom f ∈ P.valRing

theorem ArithmeticGeometry.Thm19_2.functionFieldHom_lifts_to_schemeMorphism {k : Type u} [Field k] [PerfectField k] {C₁ C₂ : SmProjCurve k} (θ : SmProjCurve.toFunctionFieldCat k C₂ ⟶ SmProjCurve.toFunctionFieldCat k C₁) : ∃ (f : C₁ ⟶ C₂), SmProjCurve.Hom.pullbackAlgHom k f = θ

theorem ArithmeticGeometry.Thm19_2.functionFieldFunctor_full (k : Type u) [Field k] [PerfectField k] : (functionFieldFunctor k).Full

theorem ArithmeticGeometry.Thm19_2.functionFieldFunctor_essSurj (k : Type u) [Field k] [PerfectField k] : (functionFieldFunctor k).EssSurj

theorem ArithmeticGeometry.Thm19_2.functionFieldFunctor_isEquivalence (k : Type u) [Field k] [PerfectField k] : (functionFieldFunctor k).IsEquivalence

noncomputable def ArithmeticGeometry.Thm19_2.curve_functionField_contravariantEquivalence (k : Type u) [Field k] [PerfectField k] : (SmProjCurve k)ᵒᵖ ≌ FunctionFieldCat k