theorem normal_variety_is_integral_closure_of_function_field (B : Type u_1) (A : Type u_2) [CommRing B] [IsDomain B] [CommRing A] [IsDomain A] [Algebra B A] [Algebra.IsIntegral B A] [IsIntegrallyClosed A] : IsIntegralClosure A B (FractionRing A)

A normal B-algebra A (integral and integrally closed) is the integral closure of B in its fraction field.

theorem normal_variety_reconstruction_unique (B : Type u_1) (A : Type u_2) (A' : Type u_3) (K : Type u_4) [CommRing B] [IsDomain B] [CommRing A] [IsDomain A] [CommRing A'] [IsDomain A'] [CommRing K] [Algebra B K] [Algebra B A] [Algebra.IsIntegral B A] [IsIntegrallyClosed A] [Algebra A K] [IsScalarTower B A K] [Algebra B A'] [Algebra.IsIntegral B A'] [IsIntegrallyClosed A'] [Algebra A' K] [IsScalarTower B A' K] [IsFractionRing A K] [IsFractionRing A' K] : Nonempty (A ≃ₐ[B] A')

Reconstruction uniqueness: two normal B-algebras with the same field of fractions K are uniquely B-isomorphic (Cor 22, Lec 17).

noncomputable def corollary22_scheme_iso (B A A' K : Type) [CommRing B] [IsDomain B] [CommRing A] [IsDomain A] [CommRing A'] [IsDomain A'] [CommRing K] [Algebra B K] [Algebra B A] [Algebra.IsIntegral B A] [IsIntegrallyClosed A] [Algebra A K] [IsScalarTower B A K] [Algebra B A'] [Algebra.IsIntegral B A'] [IsIntegrallyClosed A'] [Algebra A' K] [IsScalarTower B A' K] [IsFractionRing A K] [IsFractionRing A' K] : AlgebraicGeometry.Spec (CommRingCat.of A') ≅ AlgebraicGeometry.Spec (CommRingCat.of A)

Scheme-theoretic form of Corollary 22 (Lec 17): Spec A ≅ Spec A' whenever A and A' are normal B-algebras with the same fraction field K.

theorem corollary22_scheme_iso_over_base (B A A' K : Type) [CommRing B] [IsDomain B] [CommRing A] [IsDomain A] [CommRing A'] [IsDomain A'] [CommRing K] [Algebra B K] [Algebra B A] [Algebra.IsIntegral B A] [IsIntegrallyClosed A] [Algebra A K] [IsScalarTower B A K] [Algebra B A'] [Algebra.IsIntegral B A'] [IsIntegrallyClosed A'] [Algebra A' K] [IsScalarTower B A' K] [IsFractionRing A K] [IsFractionRing A' K] : CategoryTheory.CategoryStruct.comp (corollary22_scheme_iso B A A' K).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap B A))) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap B A'))

The reconstruction isomorphism Spec A' ≅ Spec A is compatible with the structure morphisms to Spec B.

noncomputable def smooth_complete_curve_reconstruction (k : Type) [Field k] (A_X A_Y : Type) [CommRing A_X] [IsDomain A_X] [CommRing A_Y] [IsDomain A_Y] [Algebra k A_X] [Algebra k A_Y] [IsIntegrallyClosed A_X] [IsIntegrallyClosed A_Y] [Algebra.IsIntegral k A_X] [Algebra.IsIntegral k A_Y] (K_X K_Y : Type) [Field K_X] [Field K_Y] [Algebra A_X K_X] [IsFractionRing A_X K_X] [Algebra A_Y K_Y] [IsFractionRing A_Y K_Y] [Algebra k K_X] [IsScalarTower k A_X K_X] [Algebra k K_Y] [IsScalarTower k A_Y K_Y] (φ : K_X ≃ₐ[k] K_Y) : AlgebraicGeometry.Spec (CommRingCat.of A_Y) ≅ AlgebraicGeometry.Spec (CommRingCat.of A_X)

A smooth complete curve over k is reconstructed (up to scheme isomorphism) from its function field: a k-isomorphism K_X ≃ₐ[k] K_Y of function fields induces Spec A_Y ≅ Spec A_X.