theorem Lec6.RegularFunctions.isFraction_iff (R : Type u_1) [CommRing R] {U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)} (f : (x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations R ↑x) : AlgebraicGeometry.StructureSheaf.IsFraction f ↔ ∃ (g : R) (h : R), ∀ (x : ↥U), ∃ (hx : h ∉ (↑x).asIdeal), f x = LocalizedModule.mk g ⟨h, hx⟩

Unfolding StructureSheaf.IsFraction: a section is a fraction iff it is globally given by g/h for some g, h ∈ R with h invertible at every point of U.

theorem Lec6.RegularFunctions.stalk_eq_colimit {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (x : ↑X) : F.stalk x = (TopCat.Presheaf.stalkFunctor CommRingCat x).obj F

The stalk of a presheaf at a point is, by definition, the filtered colimit of its sections over open neighborhoods of that point.

noncomputable def Lec6.RegularFunctions.stalk_iso_localization (R : Type u_1) [CommRing R] (𝔭 : PrimeSpectrum R) : Localization.AtPrime 𝔭.asIdeal ≃ₐ[R] ↑((AlgebraicGeometry.structurePresheafInCommRingCat R).stalk 𝔭)

The stalk of the structure sheaf of Spec R at a prime 𝔭 is canonically the localization of R at 𝔭.

theorem Lec6.RegularFunctions.functionField_eq_stalk_genericPoint (X : AlgebraicGeometry.Scheme) [IrreducibleSpace ↥X] : X.functionField = X.presheaf.stalk (genericPoint ↥X)

For an irreducible scheme, the function field is defined as the stalk of the structure sheaf at the (unique) generic point.

theorem Lec6.RegularFunctions.functionField_germ_injective' (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (U : X.Opens) [Nonempty ↥↑U] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U))

On an integral scheme, the germ map from sections over a nonempty open U into the function field is injective.

@[implicit_reducible]

noncomputable instance Lec6.RegularFunctions.functionField_field' (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] : Field ↑X.functionField

The function field of an integral scheme is a field.