structure AlgebraicGeometry.CompletenessValuationCriterion.AlgVariety (k : Type u) [Field k] : Type (u + 1)

• carrier : Type u
• topInst : TopologicalSpace self.carrier
• functionField : Type u
• ffField : Field self.functionField
• baseEmbed : k →+* self.functionField
• baseEmbed_inj : Function.Injective ⇑self.baseEmbed
• localRingAt : self.carrier → Subring self.functionField
• base_le_localRing (P : self.carrier) (x : k) : self.baseEmbed x ∈ self.localRingAt P
• noethProduct (Y : Type u) [TopologicalSpace Y] [TopologicalSpace.NoetherianSpace Y] : TopologicalSpace.NoetherianSpace (self.carrier × Y)

structure AlgebraicGeometry.CompletenessValuationCriterion.SubvarietyOf {k : Type u} [Field k] (X : AlgVariety k) : Type (u + 1)

• toVariety : AlgVariety k
• inclusion : self.toVariety.carrier → X.carrier

structure AlgebraicGeometry.CompletenessValuationCriterion.ValRingOver {k : Type u} [Field k] (V : AlgVariety k) : Type u

• valSub : ValuationSubring V.functionField
• contains_base (x : k) : V.baseEmbed x ∈ self.valSub

def AlgebraicGeometry.CompletenessValuationCriterion.localRing_le {k : Type u} [Field k] {V : AlgVariety k} (P : V.carrier) (R : ValRingOver V) : Prop

def AlgebraicGeometry.CompletenessValuationCriterion.SatisfiesValuationCriterion {k : Type u} [Field k] (X : AlgVariety k) : Prop

theorem AlgebraicGeometry.CompletenessValuationCriterion.lemma_16_29 {k : Type u} [Field k] [IsAlgClosed k] {K : Type u} [Field K] (A : Subring K) (φ : ↥A →+* k) : ∃ (B : ValuationSubring K) (_ : ↑A ⊆ ↑B) (Φ : ↥B →+* k), (∀ (a : K) (ha : a ∈ A) (hb : a ∈ ↑B), Φ ⟨a, hb⟩ = φ ⟨a, ha⟩) ∧ RingHom.ker Φ = IsLocalRing.maximalIdeal ↥B ∧ Function.Surjective ⇑Φ

theorem AlgebraicGeometry.CompletenessValuationCriterion.noetherian_finite_union_irreducible {k : Type u} [Field k] (X : AlgVariety k) (Y : Type u) [TopologicalSpace Y] [TopologicalSpace.NoetherianSpace Y] (V : Set (X.carrier × Y)) (hV : IsClosed V) : ∃ (n : ℕ) (components : Fin n → Set (X.carrier × Y)), (∀ (i : Fin n), IsClosed (components i)) ∧ (∀ (i : Fin n), IsIrreducible (components i)) ∧ V = ⋃ (i : Fin n), components i

theorem AlgebraicGeometry.CompletenessValuationCriterion.isClosed_image_finite_union {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (n : ℕ) (components : Fin n → Set X) (hclosed : ∀ (i : Fin n), IsClosed (f '' components i)) : IsClosed (f '' ⋃ (i : Fin n), components i)

structure AlgebraicGeometry.CompletenessValuationCriterion.DominantProjectionData {k : Type u} [Field k] (X : AlgVariety k) (Y : Type u) [TopologicalSpace Y] (V : Set (X.carrier × Y)) : Type (u + 1)

• Z : SubvarietyOf X
• Vvar : AlgVariety k
• embed : self.Vvar.carrier → X.carrier × Y
• embed_mem (p : self.Vvar.carrier) : self.embed p ∈ V
• toZ : self.Vvar.carrier → self.Z.toVariety.carrier
• psiStar : self.Z.toVariety.functionField →+* self.Vvar.functionField
• psiStar_inj : Function.Injective ⇑self.psiStar
• psiStar_base_compat (x : k) : self.psiStar (self.Z.toVariety.baseEmbed x) = self.Vvar.baseEmbed x

theorem AlgebraicGeometry.CompletenessValuationCriterion.exists_dominant_projection_data {k : Type u} [Field k] (X : AlgVariety k) (Y : Type u) [TopologicalSpace Y] (V : Set (X.carrier × Y)) (_hV : IsClosed V) (_hVirr : IsIrreducible V) (_hVne : V.Nonempty) : Nonempty (DominantProjectionData X Y V)

theorem AlgebraicGeometry.CompletenessValuationCriterion.valuation_ring_pullback {F₁ : Type u_1} {F₂ : Type u_2} [Field F₁] [Field F₂] (ψ : F₁ →+* F₂) (_hψ : Function.Injective ⇑ψ) (S : ValuationSubring F₂) : ∃ (R : ValuationSubring F₁), ∀ (x : F₁), x ∈ R ↔ ψ x ∈ S

structure AlgebraicGeometry.CompletenessValuationCriterion.CoordRingEvalData {k : Type u} [Field k] {X : AlgVariety k} {Y : Type u} [TopologicalSpace Y] {V : Set (X.carrier × Y)} (dpd : DominantProjectionData X Y V) (Q : Y) : Type u

• coordRingY : Subring dpd.Vvar.functionField
• evalAtQ : ↥self.coordRingY →+* k
• base_le_coordRingY (x : k) : dpd.Vvar.baseEmbed x ∈ self.coordRingY
• evalAtQ_fixes_base (x : k) (hx : dpd.Vvar.baseEmbed x ∈ self.coordRingY) : self.evalAtQ ⟨dpd.Vvar.baseEmbed x, hx⟩ = x
• psiStar_base_compat (x : k) : dpd.psiStar (dpd.Z.toVariety.baseEmbed x) = dpd.Vvar.baseEmbed x

theorem AlgebraicGeometry.CompletenessValuationCriterion.exists_coord_ring_eval_data {k : Type u} [Field k] [IsAlgClosed k] {X : AlgVariety k} {Y : Type u} [TopologicalSpace Y] {V : Set (X.carrier × Y)} (dpd : DominantProjectionData X Y V) (Q : Y) : Nonempty (CoordRingEvalData dpd Q)

theorem AlgebraicGeometry.CompletenessValuationCriterion.nullstellensatz_point_from_coordring {k : Type u} [Field k] [IsAlgClosed k] {X : AlgVariety k} {Y : Type u} [TopologicalSpace Y] {V : Set (X.carrier × Y)} (dpd : DominantProjectionData X Y V) (Q : Y) (coordRingY : Subring dpd.Vvar.functionField) (evalAtQ : ↥coordRingY →+* k) (coordRingV : Subring dpd.Vvar.functionField) (hYV : ↑coordRingY ⊆ ↑coordRingV) (S : ValuationSubring dpd.Vvar.functionField) (hVS : ↑coordRingV ⊆ ↑S) (Φ : ↥S →+* k) (hΦ_ext : ∀ (a : dpd.Vvar.functionField) (ha : a ∈ coordRingY) (hb : a ∈ ↑S), Φ ⟨a, hb⟩ = evalAtQ ⟨a, ha⟩) : ∃ (p : dpd.Vvar.carrier), (dpd.embed p).2 = Q

theorem AlgebraicGeometry.CompletenessValuationCriterion.coordring_contained_in_valring {k : Type u} [Field k] [IsAlgClosed k] {X : AlgVariety k} {Y : Type u} [TopologicalSpace Y] {V : Set (X.carrier × Y)} (dpd : DominantProjectionData X Y V) (coordRingY : Subring dpd.Vvar.functionField) (S : ValuationSubring dpd.Vvar.functionField) (hAS : ↑coordRingY ⊆ ↑S) (_P₀ : dpd.Z.toVariety.carrier) (_hP₀ : ∀ x ∈ dpd.Z.toVariety.localRingAt _P₀, dpd.psiStar x ∈ S) : ∃ (coordRingV : Subring dpd.Vvar.functionField), ↑coordRingY ⊆ ↑coordRingV ∧ ↑coordRingV ⊆ ↑S

theorem AlgebraicGeometry.CompletenessValuationCriterion.hilbert_nullstellensatz_variety_point {k : Type u} [Field k] [IsAlgClosed k] {X : AlgVariety k} {Y : Type u} [TopologicalSpace Y] {V : Set (X.carrier × Y)} (dpd : DominantProjectionData X Y V) (Q : Y) (coordRingY : Subring dpd.Vvar.functionField) (evalAtQ : ↥coordRingY →+* k) (S : ValuationSubring dpd.Vvar.functionField) (hAS : ↑coordRingY ⊆ ↑S) (Φ : ↥S →+* k) (hΦ_ext : ∀ (a : dpd.Vvar.functionField) (ha : a ∈ coordRingY) (hb : a ∈ ↑S), Φ ⟨a, hb⟩ = evalAtQ ⟨a, ha⟩) (P₀ : dpd.Z.toVariety.carrier) (hP₀ : ∀ x ∈ dpd.Z.toVariety.localRingAt P₀, dpd.psiStar x ∈ S) : ∃ (p : dpd.Vvar.carrier), (dpd.embed p).2 = Q

theorem AlgebraicGeometry.CompletenessValuationCriterion.nullstellensatz_point_recovery {k : Type u} [Field k] [IsAlgClosed k] {X : AlgVariety k} {Y : Type u} [TopologicalSpace Y] {V : Set (X.carrier × Y)} (dpd : DominantProjectionData X Y V) (Q : Y) (coordRingY : Subring dpd.Vvar.functionField) (evalAtQ : ↥coordRingY →+* k) (S : ValuationSubring dpd.Vvar.functionField) (hAS : ↑coordRingY ⊆ ↑S) (Φ : ↥S →+* k) (hΦ_ext : ∀ (a : dpd.Vvar.functionField) (ha : a ∈ coordRingY) (hb : a ∈ ↑S), Φ ⟨a, hb⟩ = evalAtQ ⟨a, ha⟩) (P₀ : dpd.Z.toVariety.carrier) (hP₀ : ∀ x ∈ dpd.Z.toVariety.localRingAt P₀, dpd.psiStar x ∈ S) : ∃ (P : X.carrier), (P, Q) ∈ V

theorem AlgebraicGeometry.CompletenessValuationCriterion.point_in_V_from_valuation_data {k : Type u} [Field k] [IsAlgClosed k] (X : AlgVariety k) (Y : Type u) [TopologicalSpace Y] (V : Set (X.carrier × Y)) (hX : SatisfiesValuationCriterion X) (dpd : DominantProjectionData X Y V) (Q : Y) : ∃ (P : X.carrier), (P, Q) ∈ V

theorem AlgebraicGeometry.CompletenessValuationCriterion.irreducible_component_has_point {k : Type u} [Field k] [IsAlgClosed k] (X : AlgVariety k) (hX : SatisfiesValuationCriterion X) (Y : Type u) [TopologicalSpace Y] (V : Set (X.carrier × Y)) (hV : IsClosed V) (hVirr : IsIrreducible V) (Q : Y) (_hQ : Q ∈ closure (Prod.snd '' V)) : Q ∈ Prod.snd '' V

theorem AlgebraicGeometry.CompletenessValuationCriterion.isClosed_snd_image_of_closure_subset {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (V : Set (X × Y)) (h : closure (Prod.snd '' V) ⊆ Prod.snd '' V) : IsClosed (Prod.snd '' V)

theorem AlgebraicGeometry.CompletenessValuationCriterion.snd_image_closed_of_valuation_criterion {k : Type u} [Field k] [IsAlgClosed k] (X : AlgVariety k) (hX : SatisfiesValuationCriterion X) (Y : Type u) [TopologicalSpace Y] [TopologicalSpace.NoetherianSpace Y] (V : Set (X.carrier × Y)) (hV : IsClosed V) : IsClosed (Prod.snd '' V)

theorem AlgebraicGeometry.CompletenessValuationCriterion.completeness_valuation_criterion {k : Type u} [Field k] [IsAlgClosed k] (X : AlgVariety k) (hX : SatisfiesValuationCriterion X) : IsCompleteVariety X.carrier