LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

`AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen` theorem AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))), IsUnit ((X.toToΓSpecMapBasicOpen r) r) The theorem `AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen` states that for any Locally Ringed Space `X` and any global section `r`, the restriction of `r` to the basic open set defined by `r` itself is a unit. Here, a unit means that it has a two-sided inverse in the monoid of the ringed space. In other words, in the context of algebraic geometry, the function `r` is invertible when restricted to the subset of the space where `r` does not vanish. More concisely: For any Locally Ringed Space X and global section r, the restriction of r to the basic open set {s : X \| r(s) ≠ 0} is a unit in the ring of functions on X.
`AlgebraicGeometry.ΓSpec.right_triangle` theorem AlgebraicGeometry.ΓSpec.right_triangle : ∀ (R : CommRingCat), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.identityToΓSpec.app (AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))) (AlgebraicGeometry.Spec.toLocallyRingedSpace.map (AlgebraicGeometry.SpecΓIdentity.inv.app R).op) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id AlgebraicGeometry.LocallyRingedSpace).obj (AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))) This theorem, `AlgebraicGeometry.ΓSpec.right_triangle`, states that for any commutative ring `R` in the category of commutative rings (`CommRingCat`), the composition of the application of the identity transformation to `ΓSpec` and the mapping of the inverse application of `SpecΓIdentity` is the same as the identity on the object of the identity functor applied to the locally ringed space of the spectrum of `R`. This represents the right triangle identity in the adjunction between the global sections functor `Γ` and the spectrum functor `Spec`. In simpler terms, it's saying that a certain round-trip process (first applying `ΓSpec` and then applying `SpecΓIdentity`) is essentially the same as doing nothing at all to the commutative ring `R`. More concisely: For any commutative ring R in the category of commutative rings, the composition of `ΓSpec` and `SpecΓIdentity` is equal to the identity functor on the spectrum of R.
`AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec` theorem AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑X.toTopCat), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (↑(Opposite.op (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))).unop) (X.toΓSpecSheafedSpace.base x)) (AlgebraicGeometry.PresheafedSpace.stalkMap X.toΓSpecSheafedSpace x) = X.ΓToStalk x This theorem states that for any locally ringed space `X` and any point `x` in the underlying topological space of `X`, the composition of the canonical ring homomorphism (which interprets an element of `R` as an element of the stalk of the structure sheaf of `R` at `x`) and the stalk map (which is induced by the unit and maps from the global sections `Γ(X)` to the stalks both in the spectrum of `Γ(X)` and in `X` itself), is equivalent to the map from the global sections to the stalk at `x`. In simpler terms, this statement expresses a fundamental property of the structure of locally ringed spaces, namely that certain natural maps involving the global sections and the stalks at a point are compatible in a specific sense. More concisely: The canonical homomorphism from a locally ringed space's global sections to its stalks at a point is equal to the restriction map from the global sections to that stalk.
`AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq` theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))), X.toΓSpecMapBasicOpen r = X.toRingedSpace.basicOpen r The theorem `AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq` states that for any locally ringed space 'X' and any element 'r' in the global sections of 'X' (denoted as Γ(X)), the preimage (through the map to the spectrum of the ring of global sections) that is the basic open set in 'X' defined by the element 'r' is equal to the basic open set in the ringed space 'X' defined by the same element 'r'. This establishes a correspondence between certain open subsets of 'X' and its ring of global sections. More concisely: For any locally ringed space X and element r in Γ(X), the basic open set in X defined by r for the topology of X coincides with the basic open set in the algebra of global sections of X defined by r.
`AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle` theorem AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle : ∀ (X : AlgebraicGeometry.LocallyRingedSpace), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.toSpecΓ (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) (X.toΓSpec.val.c.app (Opposite.op ⊤)) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)) The theorem `AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle` states that for any Locally Ringed Space `X`, the composition of the morphism `toSpecΓ _` applied to the global sections of `X` and the morphism from `X` to its Spec, when evaluated at `⊤`, is equal to the identity on the global sections of `X`. In simpler terms, it shows that these two operations -- taking global sections then moving to the Spec, and staying in `X` -- are essentially the same, and constitute mutually inverse processes in the category of Locally Ringed Spaces. This is a key part of the correspondence between algebraic geometry and commutative algebra. More concisely: For any Locally Ringed Space X, the composition of `toSpecΓ X.globalFunctions` and the structural morphism X → Spec X evaluated at the identity function id\_X equals the identity function on X.globalFunctions.
`AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff` theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) (f : (AlgebraicGeometry.Spec.structureSheaf ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))).val.obj (Opposite.op (PrimeSpectrum.basicOpen r)) ⟶ X.presheaf.obj (Opposite.op (X.toΓSpecMapBasicOpen r))), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) (PrimeSpectrum.basicOpen r)) f = X.toToΓSpecMapBasicOpen r ↔ f = X.toΓSpecCApp r This theorem provides a characterization of the sheaf homomorphism on basic opens. Given a locally ringed space X and an element r of the global sections of X, it states that for any morphism f from the structure sheaf on the spectrum of the global sections of X at the basic open defined by r to the presheaf of X at the basic open mapped by X's structure morphism to the spectrum using r, the composition of the canonical ring homomorphism interpreting an element of the global sections of X as a section of the structure sheaf with f equals the morphism associated with X and r if and only if f equals the morphism associated with X and r in the category of locally ringed spaces. More concisely: Given a locally ringed space X and an element r in its global sections, the canonical homomorphism from the section r as a global section to the structure sheaf on the basic open defined by r is equal to the associated morphism from X to the presheaf at that open if and only if both morphisms are equal in the category of locally ringed spaces.
`AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preim_basicOpen_eq` theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preim_basicOpen_eq : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))), X.toΓSpecFun ⁻¹' (PrimeSpectrum.basicOpen r).carrier = (X.toRingedSpace.basicOpen r).carrier This theorem states that for any locally ringed space `X` and any element `r` in the global sections of `X`, the preimage of a basic open set in the spectrum of the global sections of `X` (denoted by `Spec Γ(X)`) under the structure map to the spectrum (often called the "unit") is exactly the basic open set in `X` defined by the same element. In other words, these two sets, the preimage and the basic open set, are equal as sets. Here, a basic open set in a ringed space is defined by an element of the ring and it contains all the prime ideals that do not contain this element. The spectrum of a ring, `Spec R`, is a space whose points correspond to the prime ideals of `R`. This theorem is essentially saying that the structure map to the spectrum respects this notion of basic open sets. More concisely: For any locally ringed space `X` and any element `r` in the global sections of `X`, the preimage of the basic open set in `Spec Γ(X)` defined by `r` under the structure map is equal to the basic open set in `X` defined by `r`.
`AlgebraicGeometry.LocallyRingedSpace.toΓSpec_continuous` theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_continuous : ∀ (X : AlgebraicGeometry.LocallyRingedSpace), Continuous X.toΓSpecFun This theorem states that for any given locally ringed space `X` in Algebraic Geometry, the function `toΓSpecFun` associated with `X` is continuous. In the context of algebraic geometry, locally ringed spaces are a generalization of schemes, and the `toΓSpecFun` function can typically be understood as mapping a locally ringed space to its global sections. The continuity of this function is an important property in the study of these mathematical structures. More concisely: The `toΓSpecFun` function from the locally ringed space `X` in algebraic geometry is continuous.