theorem ArithmeticGeometry.dvr_isInteger_or_isInteger {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : K) : IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

theorem ArithmeticGeometry.dvr_exists_normalizer {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {n : ℕ} (f : Fin (n + 1) → K) (hne : ∃ (i : Fin (n + 1)), f i ≠ 0) : ∃ (j : Fin (n + 1)), f j ≠ 0 ∧ ∀ (i : Fin (n + 1)), IsLocalization.IsInteger R (f i * (f j)⁻¹)

structure ArithmeticGeometry.RationalMapToProj (K : Type u_1) [Field K] (n : ℕ) : Type u_1

• coords : Fin (n + 1) → K
• coords_ne_zero : ∃ (i : Fin (n + 1)), self.coords i ≠ 0

def ArithmeticGeometry.RationalMapToProj.IsRegularAt {K : Type u_1} [Field K] {n : ℕ} (φ : RationalMapToProj K n) (R : Type u_2) [CommRing R] [IsDomain R] [Algebra R K] [IsFractionRing R K] : Prop

def ArithmeticGeometry.RationalMapToProj.ExtendsMorphism {K : Type u_1} [Field K] {n : ℕ} (φ : RationalMapToProj K n) {P : Type u_2} (R : P → Type u_3) [(p : P) → CommRing (R p)] [∀ (p : P), IsDomain (R p)] [(p : P) → Algebra (R p) K] [∀ (p : P), IsFractionRing (R p) K] : Prop

structure ArithmeticGeometry.MorphismToProj (K : Type u_1) [Field K] (n : ℕ) {P : Type u_2} (R : P → Type u_3) [(p : P) → CommRing (R p)] [∀ (p : P), IsDomain (R p)] [(p : P) → Algebra (R p) K] [∀ (p : P), IsFractionRing (R p) K] : Type u_1

• toRationalMap : RationalMapToProj K n
• is_morphism : self.toRationalMap.ExtendsMorphism R

theorem ArithmeticGeometry.RationalMapToProj.isRegularAt_of_isDVR {K : Type u_1} [Field K] {n : ℕ} (φ : RationalMapToProj K n) (R : Type u_2) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Algebra R K] [IsFractionRing R K] : φ.IsRegularAt R

theorem ArithmeticGeometry.SmoothProjectiveCurve.rational_map_is_morphism {K : Type u_1} [Field K] {P : Type u_2} {n : ℕ} (φ : RationalMapToProj K n) (R : P → Type u_3) [(p : P) → CommRing (R p)] [∀ (p : P), IsDomain (R p)] [∀ (p : P), IsDiscreteValuationRing (R p)] [(p : P) → Algebra (R p) K] [∀ (p : P), IsFractionRing (R p) K] : φ.ExtendsMorphism R

def ArithmeticGeometry.SmoothProjectiveCurve.rational_map_extends_to_morphism {K : Type u_1} [Field K] {P : Type u_2} {n : ℕ} (φ : RationalMapToProj K n) (R : P → Type u_3) [(p : P) → CommRing (R p)] [∀ (p : P), IsDomain (R p)] [∀ (p : P), IsDiscreteValuationRing (R p)] [(p : P) → Algebra (R p) K] [∀ (p : P), IsFractionRing (R p) K] : MorphismToProj K n R

structure ArithmeticGeometry.RationalMapToProjectiveVariety (K : Type u_1) [Field K] (n : ℕ) (V : Set (Fin (n + 1) → K)) extends ArithmeticGeometry.RationalMapToProj K n : Type u_1

• coords : Fin (n + 1) → K
• coords_ne_zero : ∃ (i : Fin (n + 1)), self.coords i ≠ 0

def ArithmeticGeometry.RationalMapToProjectiveVariety.IsMorphism {K : Type u_1} [Field K] {n : ℕ} {V : Set (Fin (n + 1) → K)} (φ : RationalMapToProjectiveVariety K n V) {P : Type u_2} (R : P → Type u_3) [(p : P) → CommRing (R p)] [∀ (p : P), IsDomain (R p)] [(p : P) → Algebra (R p) K] [∀ (p : P), IsFractionRing (R p) K] : Prop

theorem ArithmeticGeometry.SmoothProjectiveCurve.rational_map_to_projective_variety_is_morphism {K : Type u_1} [Field K] {P : Type u_2} {n : ℕ} {V : Set (Fin (n + 1) → K)} (φ : RationalMapToProjectiveVariety K n V) (R : P → Type u_3) [(p : P) → CommRing (R p)] [∀ (p : P), IsDomain (R p)] [∀ (p : P), IsDiscreteValuationRing (R p)] [(p : P) → Algebra (R p) K] [∀ (p : P), IsFractionRing (R p) K] : φ.IsMorphism R

structure ArithmeticGeometry.SmoothProjectiveCurveData (k : Type u) [Field k] (K : Type u) [Field K] [Algebra k K] (n : ℕ) : Type (u + 1)

• P : Type u
• R : self.P → Type u
• instCR (p : self.P) : CommRing (self.R p)
• instID (p : self.P) : IsDomain (self.R p)
• instDVR (p : self.P) : IsDiscreteValuationRing (self.R p)
• instAlg (p : self.P) : Algebra (self.R p) K
• instFR (p : self.P) : IsFractionRing (self.R p) K
• instAlgKR (p : self.P) : Algebra k (self.R p)
• instScalarTower (p : self.P) : IsScalarTower k (self.R p) K
• emb : Fin (n + 1) → K
• emb_ne_zero : ∃ (i : Fin (n + 1)), self.emb i ≠ 0
• n_pos : n ≥ 1
• emb_injective : Function.Injective self.emb
• point_nonempty : Nonempty self.P
• localRing_injective (p₁ p₂ : self.P) : (algebraMap (self.R p₁) K).range = (algebraMap (self.R p₂) K).range → p₁ = p₂
• localRing_surjective (V : ValuationSubring K) [IsDiscreteValuationRing ↥V] [IsFractionRing (↥V) K] : ∃ (p : self.P), (algebraMap (self.R p) K).range = V.toSubring

def ArithmeticGeometry.DVRDominates {K₁ : Type u_1} {K₂ : Type u_2} [Field K₁] [Field K₂] (φ_star : K₂ →+* K₁) (R₁ : Type u_3) [CommRing R₁] [IsDomain R₁] [Algebra R₁ K₁] [IsFractionRing R₁ K₁] (R₂ : Type u_4) [CommRing R₂] [IsDomain R₂] [Algebra R₂ K₂] [IsFractionRing R₂ K₂] : Prop

def ArithmeticGeometry.IsConstantFieldHom {k : Type u_1} {K₁ : Type u_2} {K₂ : Type u_3} [Field k] [Field K₁] [Field K₂] [Algebra k K₁] [Algebra k K₂] (φ_star : K₂ →ₐ[k] K₁) : Prop

def ArithmeticGeometry.IsSurjectiveOnPoints {k : Type u_1} {K₁ : Type u_2} {K₂ : Type u_3} [Field k] [Field K₁] [Field K₂] [Algebra k K₁] [Algebra k K₂] (φ_star : K₂ →ₐ[k] K₁) {P₁ : Type u_4} (R₁ : P₁ → Type u_5) [(p : P₁) → CommRing (R₁ p)] [∀ (p : P₁), IsDomain (R₁ p)] [(p : P₁) → Algebra (R₁ p) K₁] [∀ (p : P₁), IsFractionRing (R₁ p) K₁] {P₂ : Type u_6} (R₂ : P₂ → Type u_7) [(p : P₂) → CommRing (R₂ p)] [∀ (p : P₂), IsDomain (R₂ p)] [(p : P₂) → Algebra (R₂ p) K₂] [∀ (p : P₂), IsFractionRing (R₂ p) K₂] : Prop

theorem ArithmeticGeometry.morphism_constant_or_surjective_proof {k : Type u} [Field k] {K₁ K₂ : Type u} [Field K₁] [Field K₂] [Algebra k K₁] [Algebra k K₂] {n₁ : ℕ} (C₁ : SmoothProjectiveCurveData k K₁ n₁) {n₂ : ℕ} (C₂ : SmoothProjectiveCurveData k K₂ n₂) (φ_star : K₂ →ₐ[k] K₁) : IsConstantFieldHom φ_star ∨ IsSurjectiveOnPoints φ_star C₁.R C₂.R

theorem ArithmeticGeometry.SmoothProjectiveCurve.morphism_constant_or_surjective {k : Type u} [Field k] {K₁ K₂ : Type u} [Field K₁] [Field K₂] [Algebra k K₁] [Algebra k K₂] {n₁ : ℕ} (C₁ : SmoothProjectiveCurveData k K₁ n₁) {n₂ : ℕ} (C₂ : SmoothProjectiveCurveData k K₂ n₂) (φ_star : K₂ →ₐ[k] K₁) : IsConstantFieldHom φ_star ∨ IsSurjectiveOnPoints φ_star C₁.R C₂.R

structure ArithmeticGeometry.BiratIso {k K₁ K₂ : Type u} [Field k] [Field K₁] [Algebra k K₁] {n₁ : ℕ} (C₁ : SmoothProjectiveCurveData k K₁ n₁) [Field K₂] [Algebra k K₂] {n₂ : ℕ} (C₂ : SmoothProjectiveCurveData k K₂ n₂) : Type u

• σ : K₁ ≃+* K₂
• forward : RationalMapToProj K₁ n₂
• backward : RationalMapToProj K₂ n₁
• forward_inverse : ∃ (c₁ : K₁), c₁ ≠ 0 ∧ ∀ (i : Fin (n₁ + 1)), self.σ.symm (self.backward.coords i) = c₁ * C₁.emb i
• backward_inverse : ∃ (c₂ : K₂), c₂ ≠ 0 ∧ ∀ (i : Fin (n₂ + 1)), self.σ (self.forward.coords i) = c₂ * C₂.emb i

structure ArithmeticGeometry.CurveIso {k K₁ K₂ : Type u} [Field k] [Field K₁] [Algebra k K₁] {n₁ : ℕ} (C₁ : SmoothProjectiveCurveData k K₁ n₁) [Field K₂] [Algebra k K₂] {n₂ : ℕ} (C₂ : SmoothProjectiveCurveData k K₂ n₂) : Type u

• σ : K₁ ≃+* K₂
• forward : RationalMapToProj K₁ n₂
• backward : RationalMapToProj K₂ n₁
• forward_regular (p : C₁.P) : self.forward.IsRegularAt (C₁.R p)
• backward_regular (p : C₂.P) : self.backward.IsRegularAt (C₂.R p)
• forward_inverse : ∃ (c₁ : K₁), c₁ ≠ 0 ∧ ∀ (i : Fin (n₁ + 1)), self.σ.symm (self.backward.coords i) = c₁ * C₁.emb i
• backward_inverse : ∃ (c₂ : K₂), c₂ ≠ 0 ∧ ∀ (i : Fin (n₂ + 1)), self.σ (self.forward.coords i) = c₂ * C₂.emb i

def ArithmeticGeometry.SmoothProjectiveCurve.birational_map_is_isomorphism {k K₁ K₂ : Type u} [Field k] [Field K₁] [Algebra k K₁] {n₁ : ℕ} {C₁ : SmoothProjectiveCurveData k K₁ n₁} [Field K₂] [Algebra k K₂] {n₂ : ℕ} {C₂ : SmoothProjectiveCurveData k K₂ n₂} (Φ : BiratIso C₁ C₂) : CurveIso C₁ C₂

theorem ArithmeticGeometry.FunctionField_k.Subfield.eq_top_of_finrank_eq_one {F : Type u_4} [Field F] (K : Subfield F) (h : Module.finrank (↥K) F = 1) : K = ⊤

theorem ArithmeticGeometry.FunctionField_k.finrank_eq_one_of_subfield_eq_top {F : Type u_4} [Field F] (K : Subfield F) (h : K = ⊤) : Module.finrank (↥K) F = 1

theorem ArithmeticGeometry.FunctionField_k.Morphism.isIso_iff_degree_eq_one {F₁ : Type u_2} {F₂ : Type u_3} [Field F₁] [Field F₂] (φ : F₂ →+* F₁) : Function.Surjective ⇑φ ↔ degree φ = 1

def ArithmeticGeometry.localizationSubalgebraCarrier {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (S : Subalgebra k F) [IsFractionRing (↥S) F] (𝔭 : Ideal ↥S) [𝔭.IsPrime] : Set F

theorem ArithmeticGeometry.dvr_valuation_subring_eq_of_le {K : Type u_3} [Field K] {R₁ R₂ : ValuationSubring K} [IsDiscreteValuationRing ↥R₁] [IsDiscreteValuationRing ↥R₂] (hle : R₁ ≤ R₂) : R₁ = R₂

theorem ArithmeticGeometry.Subalgebra.inv_mem_of_isUnit' {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {R : Subalgebra k F} {x : F} (hx : x ∈ ↑R) (hu : IsUnit ⟨x, hx⟩) : x⁻¹ ∈ ↑R

theorem ArithmeticGeometry.localization_subset_of_complement_units {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (S R : Subalgebra k F) [IsFractionRing (↥S) F] (𝔭 : Ideal ↥S) [𝔭.IsPrime] (hSR : S ≤ R) (hunit : ∀ (b : ↥𝔭.primeCompl), IsUnit ⟨(algebraMap (↥S) F) ↑b, ⋯⟩) : localizationSubalgebraCarrier S 𝔭 ⊆ ↑R

def ArithmeticGeometry.dvrSubalgebraToValuationSubring {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (R : Subalgebra k F) [IsDomain ↥R] [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) F] : ValuationSubring F

instance ArithmeticGeometry.dvrSubalgebraToValuationSubring_isDVR {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (R : Subalgebra k F) [IsDomain ↥R] [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) F] : IsDiscreteValuationRing ↥(dvrSubalgebraToValuationSubring R)

theorem ArithmeticGeometry.dvr_subalgebra_set_eq_of_subset {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (R₁ R₂ : Subalgebra k F) [IsDomain ↥R₁] [IsDiscreteValuationRing ↥R₁] [IsFractionRing (↥R₁) F] [IsDomain ↥R₂] [IsDiscreteValuationRing ↥R₂] [IsFractionRing (↥R₂) F] (h : ↑R₁ ⊆ ↑R₂) : ↑R₁ = ↑R₂

theorem ArithmeticGeometry.adjoin_image_inv_or_self_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (S : Set F) (f : F → F) (hf : ∀ x ∈ S, f x = x ∨ f x = x⁻¹) : IntermediateField.adjoin k (f '' S) = IntermediateField.adjoin k S

theorem ArithmeticGeometry.exists_generators_in_dvr {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (R : Subalgebra k F) [IsDomain ↥R] [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) F] (S : Set F) (hS_fin : S.Finite) (hS_gen : IntermediateField.adjoin k S = ⊤) : ∃ (T : Set F), T.Finite ∧ (∀ t ∈ T, t ∈ ↑R) ∧ IntermediateField.adjoin k T = ⊤

theorem ArithmeticGeometry.isFractionRing_adjoin_of_field_generators {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] (T : Set F) (hT_gen : IntermediateField.adjoin k T = ⊤) : IsFractionRing (↥(Algebra.adjoin k T)) F

theorem ArithmeticGeometry.exists_generators_in_dvr_of_function_field {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] [FunctionField_k k F] (R : Subalgebra k F) [IsDomain ↥R] [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) F] : ∃ (T : Set F), T.Finite ∧ (∀ t ∈ T, t ∈ ↑R) ∧ IntermediateField.adjoin k T = ⊤

theorem ArithmeticGeometry.dimensionLEOne_adjoin_of_function_field {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] [FunctionField_k k F] (T : Set F) (hT_fin : T.Finite) (hT_gen : IntermediateField.adjoin k T = ⊤) : Ring.DimensionLEOne ↥(Algebra.adjoin k T)

theorem ArithmeticGeometry.isIntegrallyClosed_adjoin_of_function_field_in_dvr {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] [FunctionField_k k F] (R : Subalgebra k F) [IsDomain ↥R] [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) F] (T : Set F) (hT_fin : T.Finite) (hT_gen : IntermediateField.adjoin k T = ⊤) (hT_in_R : ∀ x ∈ T, x ∈ ↑R) {x : F} : IsIntegral (↥(Algebra.adjoin k T)) x → ∃ (y : ↥(Algebra.adjoin k T)), (algebraMap (↥(Algebra.adjoin k T)) F) y = x

theorem ArithmeticGeometry.isDedekindDomain_adjoin_of_function_field_in_dvr {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] [FunctionField_k k F] (R : Subalgebra k F) [IsDomain ↥R] [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) F] (T : Set F) (hT_fin : T.Finite) (hT_gen : IntermediateField.adjoin k T = ⊤) (hT_in_R : ∀ x ∈ T, x ∈ ↑R) : IsDedekindDomain ↥(Algebra.adjoin k T)

theorem ArithmeticGeometry.noether_normalization_for_function_fields {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] [FunctionField_k k F] (R : Subalgebra k F) [IsDomain ↥R] [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) F] (t : F) (ht : t ∈ R) : ∃ (S : Subalgebra k F) (_ : Algebra.FiniteType k ↥S) (_ : IsDedekindDomain ↥S) (_ : IsFractionRing (↥S) F), k[t] ≤ S ∧ S ≤ R

theorem ArithmeticGeometry.coordinate_ring_of_dvr {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] [FunctionField_k k F] (R : Subalgebra k F) [IsDomain ↥R] [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) F] : ∃ (S : Subalgebra k F) (_ : Algebra.FiniteType k ↥S) (_ : IsDedekindDomain ↥S) (_ : IsFractionRing (↥S) F), ¬IsField ↥S ∧ S ≤ R

theorem ArithmeticGeometry.exists_maximal_with_complement_units {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] [FunctionField_k k F] (R : Subalgebra k F) [IsDomain ↥R] [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) F] (S : Subalgebra k F) [IsDedekindDomain ↥S] [IsFractionRing (↥S) F] (hSR : S ≤ R) : ∃ (𝔭 : Ideal ↥S) (x : 𝔭.IsMaximal), ∀ (b : ↥𝔭.primeCompl), IsUnit ⟨(algebraMap (↥S) F) ↑b, ⋯⟩

theorem ArithmeticGeometry.localization_embeds_as_dvr_subalgebra {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] (S : Subalgebra k F) [IsDedekindDomain ↥S] (hfrac : IsFractionRing (↥S) F) (hnotfield : ¬IsField ↥S) (𝔭 : Ideal ↥S) (hmax : 𝔭.IsMaximal) : ∃ (L : Subalgebra k F) (x : IsDomain ↥L) (_ : IsDiscreteValuationRing ↥L) (_ : IsFractionRing (↥L) F), ↑L = localizationSubalgebraCarrier S 𝔭

theorem ArithmeticGeometry.exists_dedekind_subalgebra_with_complement_units {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] [FunctionField_k k F] (R : Subalgebra k F) [IsDomain ↥R] [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) F] : ∃ (S : Subalgebra k F) (_ : Algebra.FiniteType k ↥S) (_ : IsDedekindDomain ↥S) (hfrac : IsFractionRing (↥S) F), ¬IsField ↥S ∧ S ≤ R ∧ ∃ (𝔭 : Ideal ↥S) (hmax : 𝔭.IsMaximal) (L : Subalgebra k F) (x : IsDomain ↥L) (_ : IsDiscreteValuationRing ↥L) (_ : IsFractionRing (↥L) F), ↑L = localizationSubalgebraCarrier S 𝔭 ∧ ↑L ⊆ ↑R

theorem ArithmeticGeometry.exists_smooth_affine_curve_of_DVR {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [FunctionField_k k F] (R : Subalgebra k F) [IsDomain ↥R] [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) F] : ∃ (S : Subalgebra k F) (_ : Algebra.FiniteType k ↥S) (_ : IsDedekindDomain ↥S) (hfrac : IsFractionRing (↥S) F), ¬IsField ↥S ∧ S ≤ R ∧ ∃ (𝔭 : Ideal ↥S) (x : 𝔭.IsMaximal), ↑R = localizationSubalgebraCarrier S 𝔭

structure ArithmeticGeometry.DVROfFunctionField (k : Type u_5) (F : Type u_6) [Field k] [Field F] [Algebra k F] : Type u_6

• valRing : ValuationSubring F
• contains_k (a : k) : (algebraMap k F) a ∈ self.valRing
• isDVR : IsDiscreteValuationRing ↥self.valRing
• isFractionRing : IsFractionRing (↥self.valRing) F

def ArithmeticGeometry.DVROfFunctionField.localRing {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] (P : DVROfFunctionField k F) : ValuationSubring F

def ArithmeticGeometry.DVROfFunctionField.vanishesAt {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] (P : DVROfFunctionField k F) (f : F) : Prop

def ArithmeticGeometry.AbstractCurve.regularFunctions {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] (U : Set (DVROfFunctionField k F)) : Subring F

def ArithmeticGeometry.AbstractCurve.zeroLocus {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] (S : Set F) : Set (DVROfFunctionField k F)

@[implicit_reducible]

instance ArithmeticGeometry.AbstractCurve.zariskiTopology {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] : TopologicalSpace (DVROfFunctionField k F)

structure ArithmeticGeometry.AbstractCurve (k : Type u_5) (F : Type u_6) [Field k] [Field F] [Algebra k F] : Type u_6

• finitelyGenerated : ⊤.FG
• transcendenceDegreeOne : ∃ (x : F), Transcendental k x ∧ Algebra.IsAlgebraic (↥k⟮x⟯) F
• algClosedInF (x : F) : IsAlgebraic k x → x ∈ ⊥
• topology : TopologicalSpace (DVROfFunctionField k F)

@[reducible]

def ArithmeticGeometry.AbstractCurve.toFunctionField_k {k : Type u_5} {F : Type u_6} [Field k] [Field F] [Algebra k F] (C : AbstractCurve k F) : FunctionField_k k F

def ArithmeticGeometry.AbstractCurve.ofFunctionField_k (k : Type u_5) (F : Type u_6) [Field k] [Field F] [Algebra k F] [h : FunctionField_k k F] : AbstractCurve k F

theorem ArithmeticGeometry.AbstractCurve.regularFunctions_mem {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] (U : Set (DVROfFunctionField k F)) (f : ↥(regularFunctions U)) (P : DVROfFunctionField k F) (hP : P ∈ U) : ↑f ∈ P.valRing

theorem ArithmeticGeometry.AbstractCurve.globalRegularFunctions_eq {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] : (regularFunctions Set.univ).carrier = {f : F | ∀ (P : DVROfFunctionField k F), f ∈ P.valRing}

structure ArithmeticGeometry.AbstractCurveMorphism (k : Type u_5) (F₁ : Type u_6) (F₂ : Type u_7) [Field k] [Field F₁] [Field F₂] [Algebra k F₁] [Algebra k F₂] : Type (max u_6 u_7)

• toFun : DVROfFunctionField k F₁ → DVROfFunctionField k F₂
• pullback : F₂ →+* F₁
• pullback_comp (a : k) : self.pullback ((algebraMap k F₂) a) = (algebraMap k F₁) a
• pullback_regular (P : DVROfFunctionField k F₁) (f : F₂) : f ∈ (self.toFun P).valRing → self.pullback f ∈ P.valRing

theorem ArithmeticGeometry.AbstractCurveMorphism.pullback_regular_on_open {k : Type u_5} {F₁ : Type u_6} {F₂ : Type u_7} [Field k] [Field F₁] [Field F₂] [Algebra k F₁] [Algebra k F₂] (φ : AbstractCurveMorphism k F₁ F₂) (U : Set (DVROfFunctionField k F₂)) (f : F₂) (hf : ∀ P ∈ U, f ∈ P.valRing) (Q : DVROfFunctionField k F₁) : Q ∈ φ.toFun ⁻¹' U → φ.pullback f ∈ Q.valRing

noncomputable def ArithmeticGeometry.SmoothProjectiveCurveData.pointValSubring {k K : Type u} [Field k] [Field K] [Algebra k K] {n : ℕ} (C : SmoothProjectiveCurveData k K n) (p : C.P) : ValuationSubring K

instance ArithmeticGeometry.SmoothProjectiveCurveData.pointValSubring_isDVR {k K : Type u} [Field k] [Field K] [Algebra k K] {n : ℕ} (C : SmoothProjectiveCurveData k K n) (p : C.P) : IsDiscreteValuationRing ↥(C.pointValSubring p)

theorem ArithmeticGeometry.SmoothProjectiveCurveData.contains_k {k K : Type u} [Field k] [Field K] [Algebra k K] {n : ℕ} (C : SmoothProjectiveCurveData k K n) (p : C.P) (a : k) : (algebraMap k K) a ∈ C.pointValSubring p

noncomputable def ArithmeticGeometry.SmoothProjectiveCurveData.pointToDVR {k K : Type u} [Field k] [Field K] [Algebra k K] {n : ℕ} (C : SmoothProjectiveCurveData k K n) (p : C.P) : DVROfFunctionField k K

theorem ArithmeticGeometry.SmoothProjectiveCurveData.pointToDVR_injective {k K : Type u} [Field k] [Field K] [Algebra k K] {n : ℕ} (C : SmoothProjectiveCurveData k K n) : Function.Injective C.pointToDVR

theorem ArithmeticGeometry.SmoothProjectiveCurveData.pointToDVR_surjective {k K : Type u} [Field k] [Field K] [Algebra k K] {n : ℕ} (C : SmoothProjectiveCurveData k K n) : Function.Surjective C.pointToDVR

def ArithmeticGeometry.SmoothProjectiveCurveData.vanishesAt {k K : Type u} [Field k] [Field K] [Algebra k K] {n : ℕ} (C : SmoothProjectiveCurveData k K n) (p : C.P) (f : K) : Prop

def ArithmeticGeometry.SmoothProjectiveCurveData.zariskiTopology {k K : Type u} [Field k] [Field K] [Algebra k K] {n : ℕ} (C : SmoothProjectiveCurveData k K n) : TopologicalSpace C.P

def ArithmeticGeometry.SmoothProjectiveCurveData.regularFunctions {k K : Type u} [Field k] [Field K] [Algebra k K] {n : ℕ} (C : SmoothProjectiveCurveData k K n) (U : Set C.P) : Set K

structure ArithmeticGeometry.AbstractCurveIsomorphism {k K : Type u} [Field k] [Field K] [Algebra k K] {n : ℕ} (C : SmoothProjectiveCurveData k K n) : Type u

• pointEquiv : C.P ≃ DVROfFunctionField k K
• localRing_compat (p : C.P) : Set.range ⇑(algebraMap (C.R p) K) = ↑(self.pointEquiv p).valRing
• forward_continuous : Continuous ⇑self.pointEquiv
• regularFunctions_compat (U : Set (DVROfFunctionField k K)) : (AbstractCurve.regularFunctions U).carrier = C.regularFunctions (⇑self.pointEquiv.symm '' U)

theorem ArithmeticGeometry.smooth_projective_curve_isomorphic_abstract_curve {k K : Type u} [Field k] [Field K] [Algebra k K] {n : ℕ} (C : SmoothProjectiveCurveData k K n) : Nonempty (AbstractCurveIsomorphism C)

structure ArithmeticGeometry.IsAbstractCurveIsomorphism {k K : Type u} [Field k] [Field K] [Algebra k K] {n : ℕ} (C : SmoothProjectiveCurveData k K n) (φ : C.P ≃ DVROfFunctionField k K) : Prop

• localRing_eq (p : C.P) : Set.range ⇑(algebraMap (C.R p) K) = ↑(φ p).valRing
• regularFunctions_eq (U : Set C.P) (f : K) : f ∈ C.regularFunctions U ↔ f ∈ AbstractCurve.regularFunctions (⇑φ '' U)

theorem ArithmeticGeometry.smooth_projective_curve_isomorphic_abstract_curve_as_curves {k K : Type u} [Field k] [Field K] [Algebra k K] {n : ℕ} (C : SmoothProjectiveCurveData k K n) : ∃ (φ : C.P ≃ DVROfFunctionField k K), IsAbstractCurveIsomorphism C φ

instance ArithmeticGeometry.instIsDiscreteValuationRingSubtypeValuationSubring {K : Type u_3} [Field K] (p : { V : ValuationSubring K // IsDiscreteValuationRing ↥V }) : IsDiscreteValuationRing ↥↑p

theorem ArithmeticGeometry.ValuationSubring.eq_top_of_isField {K : Type u_3} [Field K] (V : ValuationSubring K) (hField : IsField ↥V) : V = ⊤

theorem ArithmeticGeometry.ValuationSubring.isDVR_of_isNoetherianRing_of_ne_top {K : Type u_3} [Field K] (V : ValuationSubring K) (hNoeth : IsNoetherianRing ↥V) (hV : V ≠ ⊤) : IsDiscreteValuationRing ↥V

theorem ArithmeticGeometry.functionField_exists_nontrivial_noetherian_valuationSubring (k : Type u_3) [Field k] (F : Type u_4) [Field F] [Algebra k F] (t : F) (ht : Transcendental k t) (halg : Algebra.IsAlgebraic (↥k⟮t⟯) F) : ∃ (V : ValuationSubring F), V ≠ ⊤ ∧ IsNoetherianRing ↥V

theorem ArithmeticGeometry.functionField_exists_DVR_valuationSubring_aux (k : Type u_3) [Field k] (F : Type u_4) [Field F] [Algebra k F] (t : F) (ht : Transcendental k t) (halg : Algebra.IsAlgebraic (↥k⟮t⟯) F) : ∃ (V : ValuationSubring F), IsDiscreteValuationRing ↥V

theorem ArithmeticGeometry.functionField_exists_DVR_valuationSubring (k : Type u_3) [Field k] (F : Type u_4) [Field F] [Algebra k F] [FunctionField_k k F] : Nonempty { V : ValuationSubring F // IsDiscreteValuationRing ↥V }

theorem ArithmeticGeometry.functionField_algebraMap_mem_DVR (k : Type u) [Field k] (F : Type u) [Field F] [Algebra k F] [FunctionField_k k F] (V : ValuationSubring F) [IsDiscreteValuationRing ↥V] (c : k) : (algebraMap k F) c ∈ V.toSubring

@[reducible]

noncomputable def ArithmeticGeometry.functionField_DVR_algebra (k : Type u) [Field k] (F : Type u) [Field F] [Algebra k F] [FunctionField_k k F] (V : ValuationSubring F) [IsDiscreteValuationRing ↥V] : Algebra k ↥V

theorem ArithmeticGeometry.functionField_DVR_isScalarTower (k : Type u) [Field k] (F : Type u) [Field F] [Algebra k F] [FunctionField_k k F] (V : ValuationSubring F) [IsDiscreteValuationRing ↥V] : IsScalarTower k (↥V) F

theorem ArithmeticGeometry.abstract_curve_is_smooth_projective (k : Type u) [Field k] (F : Type u) [Field F] [Algebra k F] [FunctionField_k k F] : ∃ (n : ℕ), Nonempty (SmoothProjectiveCurveData k F n)

theorem ArithmeticGeometry.abstract_curve_isomorphic_smooth_projective (k : Type u) [Field k] (F : Type u) [Field F] [Algebra k F] [FunctionField_k k F] : ∃ (n : ℕ) (C : SmoothProjectiveCurveData k F n) (φ : C.P ≃ DVROfFunctionField k F), ∀ (p : C.P), Set.range ⇑(algebraMap (C.R p) F) = ↑(φ p).valRing

theorem ArithmeticGeometry.unique_smooth_model_existence (k : Type u) [Field k] (F : Type u) [Field F] [Algebra k F] [FunctionField_k k F] : ∃ (n : ℕ), Nonempty (SmoothProjectiveCurveData k F n)

def ArithmeticGeometry.BiratIso.ofSameFunctionField {k F : Type u} [Field k] [Field F] [Algebra k F] {n₁ : ℕ} (C₁ : SmoothProjectiveCurveData k F n₁) {n₂ : ℕ} (C₂ : SmoothProjectiveCurveData k F n₂) : BiratIso C₁ C₂

def ArithmeticGeometry.unique_smooth_model_uniqueness {k F : Type u} [Field k] [Field F] [Algebra k F] {n₁ : ℕ} (C₁ : SmoothProjectiveCurveData k F n₁) {n₂ : ℕ} (C₂ : SmoothProjectiveCurveData k F n₂) : CurveIso C₁ C₂

theorem ArithmeticGeometry.unique_smooth_projective_model (k : Type u) [Field k] (F : Type u) [Field F] [Algebra k F] [FunctionField_k k F] : (∃ (n : ℕ), Nonempty (SmoothProjectiveCurveData k F n)) ∧ ∀ {n₁ n₂ : ℕ} (C₁ : SmoothProjectiveCurveData k F n₁) (C₂ : SmoothProjectiveCurveData k F n₂), Nonempty (CurveIso C₁ C₂)