Definitions: Mathlib.AlgebraicGeometry, part 3 of 3

the isomorphism image of f and U (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of $X$. Then the isomorphism image of $f$ and $U$ is an isomorphism of the scheme of $U$ and the scheme of the action of the functor of $f$ and $U$.

the isomorphism open range of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the isomorphism open range of $f$ is an isomorphism of $X$ and the scheme of the image of $f$.

the restriction of f and U (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of $Y$. Then the restriction of $f$ and $U$ is an isomorphism of the scheme of the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $U$ and the scheme of $U$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of $Y$. Let $V$ be an open of $X$ such that $V$ is less than or equal to the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $U$. Then $\operatorname{resLE}$ applied to $f$, $U$, $V$ and $e$ is a homomorphism of the scheme of $V$ and the scheme of $U$ defined as the composition of the homomorphism of $X$ and $e$ and the restriction of $f$ and $U$.

the stalk map of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$ such that $V$ is less than or equal to the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $U$. Let $x$ be an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {V}{x_{1}})}$. Then the stalk map of $f$ is an isomorphism of $\operatorname{mk}$ applied to the stalk map of $\operatorname{resLE}$ applied to $f$, $U$, $V$ and $e$ and $x$ and $\operatorname{mk}$ applied to the stalk map of $f$ and $x$.

the restriction of x and U (from the docstring)

Let $x$ be an open cover of $X$. Let $U$ be an open of $X$. Then the restriction of $x$ and $U$ is an open cover of the scheme of $U$.

the open cover of U (from the docstring)

Let $U$ be a function from elements of $J$ to opens of $X$. Then the open cover of $U$ is an open cover of the scheme of the supremum of the function that maps $i$ to $U$ applied to $i$.

the isomorphism of hUV (from the name)

Assume that $U \leq V$. Then the isomorphism of $\mathrm{hUV}$ is an isomorphism of the scheme of the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the inclusion of $V$ and $U$ and the scheme of $U$.

the stalk isomorphism of U and x (from the name)

Let $U$ be an open of $X$. Let $x$ be an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {U}{x_{1}})}$. Then the stalk isomorphism of $U$ and $x$ is an isomorphism of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the scheme of $U$ and $x$ and the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $x$.

the scheme of U (from the name)

Let $U$ be an open of $X$. Then the scheme of $U$ is a scheme.

the top isomorphism of U (from the name)

Let $U$ be an open of $X$. Then the top isomorphism of $U$ is an isomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the scheme of $U$ and $\operatorname{op}$ applied to the top and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$.

the inclusion of U (from the name)

Let $U$ be an open of $X$. Then the inclusion of $U$ is a homomorphism of the scheme of $U$ and $X$.

the homomorphism of X and e (from the name)

Let $X$ be a scheme. Assume that $U \leq V$. Then the homomorphism of $X$ and $e$ is a homomorphism of the scheme of $U$ and the scheme of $V$.

the isomorphism of X and e (from the name)

Let $X$ be a scheme. Assume that $\EqtMACRoH {U}{V}$. Then the isomorphism of $X$ and $e$ is an isomorphism of the scheme of $U$ and the scheme of $V$.

the open cover of X and U (from the name)

Let $X$ be a scheme. Let $U$ be a function from elements of $s$ to opens of $X$ such that $U$ is an open cover. Then the open cover of $X$ and $U$ is an open cover of $X$.

Let $X$ be a scheme. Then $\operatorname{restrictFunctor}$ applied to $X$ is a functor of the set of opens of $X$ and $\operatorname{Over}$ applied to $X$.

$\mathrm{AlgebraicGeometry\_\_Scheme\_\_restrictFunctor\_u393\_}$ is an isomorphism of the composition of the opposite of $\operatorname{restrictFunctor}$ applied to $X$ and the composition of the opposite of $\operatorname{forget}$ applied to $X$ and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_\_u393\_}$ and the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$.

Let $X$ be a scheme. Let $U$ and $V$ be opens of $X$. Then $\operatorname{restrictRestrictComm}$ applied to $X$, $U$ and $V$ is an isomorphism of the scheme of the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the inclusion of $U$ and $V$ and the scheme of the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the inclusion of $V$ and $U$.

the top isomorphism of X (from the name)

Let $X$ be a scheme. Then the top isomorphism of $X$ is an isomorphism of the scheme of the top and $X$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of $Y$. Let $V$ be an open of $X$ such that $V$ is less than or equal to the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $U$. Then $\operatorname{arrowResLEAppIso}$ applied to $f$, $U$, $V$ and $e$ is an isomorphism of $\operatorname{mk}$ applied to the application top of $\operatorname{resLE}$ applied to $f$, $U$, $V$ and $e$ and $\operatorname{mk}$ applied to $\operatorname{appLE}$ applied to $f$, $U$, $V$ and $e$.

Let $f$ be a carrier of $R$. Then $\operatorname{basicOpenIsoSpecAway}$ applied to $f$ is an isomorphism of the scheme of $\operatorname{basicOpen}$ applied to $f$ and the spectrum of $\operatorname{of}$ applied to $\operatorname{Away}$ applied to $f$.

the restriction of f and U (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of $Y$. Then the restriction of $f$ and $U$ is a homomorphism of the scheme of the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $U$ and the scheme of $U$ defined as the composition of the inverse of $\operatorname{pullbackRestrictIsoRestrict}$ applied to $f$ and $U$ and the second projection of the pullback of $f$ and the inclusion of $U$.

Let $f$ be a homomorphism of $X$ and $Y$. Assume that $\EqtMACRoH {U}{V}$. Then $\operatorname{morphismRestrictEq}$ applied to $f$ and $e$ is an isomorphism of $\operatorname{mk}$ applied to the restriction of $f$ and $U$ and $\operatorname{mk}$ applied to the restriction of $f$ and $V$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $U$ and $Y$. Then $\operatorname{morphismRestrictOpensRange}$ applied to $f$ and $g$ is an isomorphism of $\operatorname{mk}$ applied to the restriction of $f$ and the image of $g$ and $\operatorname{mk}$ applied to the second projection of the pullback of $f$ and $g$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of $Y$. Let $V$ be an open of the scheme of $U$. Then $\operatorname{morphismRestrictRestrict}$ applied to $f$, $U$ and $V$ is an isomorphism of $\operatorname{mk}$ applied to the restriction of the restriction of $f$ and $U$ and $V$ and $\operatorname{mk}$ applied to the restriction of $f$ and the action of the functor of the inclusion of $U$ and $V$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of $Y$. Let $r$ be a carrier of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and $\operatorname{op}$ applied to $U$. Then $\operatorname{morphismRestrictRestrictBasicOpen}$ applied to $f$, $U$ and $r$ is an isomorphism of $\operatorname{mk}$ applied to the restriction of the restriction of $f$ and $U$ and $\operatorname{basicOpen}$ applied to the scheme of $U$ and $\operatorname{hom}$ applied to the map of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and the opposite in $\operatorname{eqToHom}$ applied to $\mathrm{TopologicalSpace\_\_Opens\_\_isOpenEmbedding\_obj\_top}$ applied to $U$ and $r$ and $\operatorname{mk}$ applied to the restriction of $f$ and $\operatorname{basicOpen}$ applied to $Y$ and $r$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of $Y$. Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the scheme of the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $U$. Then $\operatorname{morphismRestrictStalkMap}$ applied to $f$, $U$ and $x$ is an isomorphism of $\operatorname{mk}$ applied to the stalk map of the restriction of $f$ and $U$ and $x$ and $\operatorname{mk}$ applied to the stalk map of $f$ and $x$.

Let $U$ be an open of $X$. Then $\operatorname{opensRestrict}$ applied to $U$ is an equivalence from the set of opens of the scheme of $U$ to $\SubtypeSet {V}{\mathrm{Leq} (V , U)}$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of $Y$. Then $\operatorname{pullbackRestrictIsoRestrict}$ applied to $f$ and $U$ is an isomorphism of the pullback of $f$ and the inclusion of $U$ and the scheme of the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $U$.

scheme (from the name)

The schemes are a basic type.

homomorphism of X and Y (from the name)

Let $X$ and $Y$ be schemes. Then the homomorphisms of $X$ and $Y$ are a basic type.

the homomorphism of f and U (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of $Y$. Then the homomorphism of $f$ and $U$ is a homomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and $\operatorname{op}$ applied to $U$ and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $U$ defined as the component of $\operatorname{c}$ applied to $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $\operatorname{op}$ applied to $U$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of $Y$. Let $V$ be an open of $X$ such that $V$ is less than or equal to the action of the map of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $U$. Then $\operatorname{appLE}$ applied to $f$, $U$, $V$ and $e$ is a homomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and $\operatorname{op}$ applied to $U$ and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $V$ defined as the composition of the homomorphism of $f$ and $U$ and the map of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and the opposite in the homomorphism of $e$.

the application top of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the application top of $f$ is a homomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and $\operatorname{op}$ applied to the top and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the top defined as the homomorphism of $f$ and the top.

the arrow stalk map isomorphism of f and h (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Assume that $\EqtMACRoH {x}{y}$. Then the arrow stalk map isomorphism of $f$ and $h$ is an isomorphism of $\operatorname{mk}$ applied to the stalk map of $f$ and $x$ and $\operatorname{mk}$ applied to the stalk map of $f$ and $y$.

the copy base of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a function from carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ to carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ such that $\operatorname{coe}$ applied to the homomorphism of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ is equal to $g$. Then the copy base of $f$ and $g$ is a homomorphism of $X$ and $Y$.

the homeomorphism of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the homeomorphism of $f$ is a homeomorphism of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ defined as the scheme isomorphism to homeomorphism of $\operatorname{asIso}$ applied to $f$.

the stalk map of f and x (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then the stalk map of $f$ and $x$ is a homomorphism of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ and $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and $x$ and the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $x$ defined as the stalk map of $\operatorname{toLRSHom}$ applied to $f$ and $x$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{toLRSHom}$ applied to $f$ is a homomorphism of $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{toLocallyRingedSpace}$ applied to $Y$ defined as $\operatorname{toLRSHom'}$ applied to $f$.

open of X (from the name)

Let $X$ be a scheme. Then an open of $X$ is an element of the function that maps $X$ to the set of opens of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$.

the spectrum (from the name)

The spectrum is a functor of the set of opposites of the set of categories of commutative rings and the set of schemes.

the spectrum identity (from the name)

The spectrum identity is an isomorphism of the composition of the right opposite of the spectrum and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_\_u393\_}$ and the identity of the set of categories of commutative rings defined as the spectrum identity.

Let $X$ be a scheme. Let $f$ be a carrier of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$. Then $\operatorname{basicOpen}$ applied to $X$ and $f$ is an open of $X$ defined as $\operatorname{basicOpen}$ applied to the ringed space of $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $f$.

the empty scheme (from the docstring)

The empty scheme is a scheme.

$\operatorname{forget}$ is a functor of the set of schemes and the set of sets defined as the composition of $\operatorname{forgetToTop}$ and the forgetful functor of the set of topological categories.

$\operatorname{forgetToTop}$ is a functor of the set of schemes and the set of topological categories defined as the composition of $\operatorname{forgetToLocallyRingedSpace}$ and $\operatorname{forgetToTop}$.

Let $X$ be a scheme. Then $\mathrm{AlgebraicGeometry\_\_Scheme\_\_forgetToTop\_obj\_eq\_coe}$ holds for $X$, if the action of $\operatorname{forgetToTop}$ and $X$ is equal to the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$.

Let $X$ be a scheme. Then $\mathrm{AlgebraicGeometry\_\_Scheme\_\_forget\_obj\_eq\_coe}$ holds for $X$, if the action of $\operatorname{forget}$ and $X$ is equal to the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$.

$\operatorname{fullyFaithfulForgetToLocallyRingedSpace}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{forgetToLocallyRingedSpace}$.

the homeomorphism of e (from the name)

Let $e$ be an isomorphism of $X$ and $Y$. Then the homeomorphism of $e$ is a homeomorphism of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ defined as the homeomorphism of the map isomorphism of $\operatorname{forgetToTop}$ and $e$.

the structure sheaf of X (from the docstring)

Let $X$ be a scheme. Then the structure sheaf of $X$ is a sheaf of the set of categories of commutative rings and the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ defined as the sheaf of $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$.

the zero locus of X and s (from the docstring)

Let $X$ be a scheme. Let $s$ be an element of the power set of the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$. Then the zero locus of $X$ and $s$ is an element of the power set of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ defined as the zero locus of the ringed space of $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $s$.

$\mathrm{AlgebraicGeometry\_\_Scheme\_\_\_u393\_}$ is a functor of the set of opposites of the set of schemes and the set of categories of commutative rings defined as the composition of the opposite of $\operatorname{forgetToLocallyRingedSpace}$ and $\mathrm{AlgebraicGeometry\_\_LocallyRingedSpace\_\_\_u393\_}$.

the spectrum isomorphism of R (from the name)

Let $R$ be a category of commutative rings. Then the spectrum isomorphism of $R$ is an isomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$ and $\operatorname{op}$ applied to the top and $R$ defined as the application of the spectrum identity and $R$.

the spectrum of R (from the docstring)

Let $R$ be a category of commutative rings. Then the spectrum of $R$ is a scheme.

the algebra map of R and A (from the name)

Let $R$ and $A$ be sets. Then the algebra map of $R$ and $A$ is a homomorphism of the spectrum of $\operatorname{of}$ applied to $A$ and the spectrum of $\operatorname{of}$ applied to $R$ defined as the induced map of the commutative ring category of the algebra map of $R$ and $A$.

the induced map of f (from the docstring)

Let $f$ be a homomorphism of $R$ and $S$. Then the induced map of $f$ is a homomorphism of the spectrum of $S$ and the spectrum of $R$ defined as $\operatorname{mk}$ applied to the induced map of $f$.

the prime spectrum order isomorphism spectrum of R (from the name)

Let $R$ be a set. Then the prime spectrum order isomorphism spectrum of $R$ is an order isomorphism of the set of prime spectra of $R$ and the set of order duals of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $\operatorname{of}$ applied to $R$.

the spectrum order isomorphism prime spectrum of R (from the name)

Let $R$ be a category of commutative rings. Then the spectrum order isomorphism prime spectrum of $R$ is an order isomorphism of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$ and the set of order duals of the set of prime spectra of the set of carriers of $R$.

the scheme isomorphism to homeomorphism of e (from the name)

Let $e$ be an isomorphism of $X$ and $Y$. Then the scheme isomorphism to homeomorphism of $e$ is a homeomorphism of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $Y$ defined as the homeomorphism of $e$.

Let $f$ be a homomorphism of the spectrum of $R$ and $S$ such that $P$ holds for the spectrum of $R$, $S$ and $f$. Then $\operatorname{affineOverMk}$ applied to $f$ and $\mathrm{hf}$ is a costructured arrow of the spectrum and $S$ defined as $\operatorname{mk}$ applied to the top, $f$ and $\mathrm{hf}$.

affine etale of S (from the name)

Let $S$ be a scheme. Then an affine etale of $S$ is an element of the function that maps $S$ to the set of costructured arrows of the spectrum and $S$.

the spectrum of S (from the name)

Let $S$ be a scheme. Then the spectrum of $S$ is a functor of the set of affine etales of $S$ and the set of etales of $S$ defined as $\operatorname{toOver}$ applied to the proposition that $\operatorname{Etale}$, the spectrum and $S$.

Let $f$ be a homomorphism of the spectrum of $R$ and $S$. Then $\operatorname{mk}$ applied to $f$ is an affine etale of $S$ defined as $\operatorname{mk}$ applied to the top, $f$ and $h$.

the sheaf equivalence of S and A (from the name)

Let $S$ be a scheme. Let $A$ be a set. Then the sheaf equivalence of $S$ and $A$ is an equivalence of the set of sheaves of the topology of $S$ and $A$ and the set of sheaves of the small etale topology of $S$ and $A$ defined as the inverse of $\operatorname{asEquivalence}$ applied to $\operatorname{sheafPushforwardContinuous}$ applied to the spectrum of $S$, $A$, the topology of $S$ and the small etale topology of $S$.

the topology of S (from the name)

Let $S$ be a scheme. Then the topology of $S$ is a Grothendieck topology of the set of affine etales of $S$ defined as the induced topology of the spectrum of $S$ and the small etale topology of $S$.

the affine one hypercover of X (from the name)

Let $X$ be a scheme. Then the affine one hypercover of $X$ is an one hypercover of the Zariski topology and $X$.

the Zariski pretopology (from the name)

The Zariski pretopology is a pretopology of the set of schemes defined as the pretopology of $\operatorname{IsOpenImmersion}$.

the Zariski topology (from the name)

The Zariski topology is a Grothendieck topology of the set of schemes defined as the Grothendieck topology of $\operatorname{IsOpenImmersion}$.

the continuous map presheaf of T (from the name)

Let $T$ be a set. Then the continuous map presheaf of $T$ is a functor of the set of opposites of the set of schemes and the set of sets.

the continuous map presheaf abelian group of A (from the name)

Let $A$ be a set. Then the continuous map presheaf abelian group of $A$ is a functor of the set of opposites of the set of schemes and the set of abelian groups.

Let $A$ be a set. Then $\operatorname{continuousMapPresheafAbForgetIso}$ applied to $A$ is an isomorphism of the composition of the continuous map presheaf abelian group of $A$ and the forgetful functor of the set of abelian groups and the continuous map presheaf of $A$ defined as the identity of the composition of the continuous map presheaf abelian group of $A$ and the forgetful functor of the set of abelian groups.

the continuous map presheaf equivalence of T and U (from the name)

Let $T$ be a set. Let $U$ be a scheme. Then the continuous map presheaf equivalence of $T$ and $U$ is an equivalence from the action of the continuous map presheaf of $T$ and $\operatorname{op}$ applied to $U$ to the set of continuous maps of the set of connected components of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $U$ and $T$.

the continuous map presheaf isomorphism lift of T (from the name)

Let $T$ be a set. Then the continuous map presheaf isomorphism lift of $T$ is an isomorphism of the continuous map presheaf of $T$ and the composition of the opposite of $\operatorname{forgetToTop}$ and the composition of the opposite of the lift functor and the action of the Yoneda and $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to $T$.

Let $X$ be a scheme. Let $x$ and $n$ be natural numbers. Then an element of $\operatorname{EllAdicCohomology}$ applied to $X$, $x$ and $n$ is an element of the function that maps $X$, $x$ and $n$ to $\operatorname{H}$ applied to the action of $\operatorname{sheafCompose}$ applied to the topology of $X$ and the lift functor and $\operatorname{ellAdicSheaf}$ applied to $X$ and $x$ and $n$.

Let $X$ be a scheme. Let $x$ be a natural number. Then $\operatorname{ellAdicSheaf}$ applied to $X$ and $x$ is a sheaf of the topology of $X$ and the set of abelian groups.

the etale precoverage (from the name)

The etale precoverage is a precoverage of the set of schemes defined as the precoverage of the proposition that $\operatorname{Etale}$.

the etale pretopology (from the name)

The etale pretopology is a pretopology of the set of schemes defined as the pretopology of the proposition that $\operatorname{Etale}$.

the etale topology (from the name)

The etale topology is a Grothendieck topology of the set of schemes defined as the Grothendieck topology of the proposition that $\operatorname{Etale}$.

the geometric fiber of x (from the name)

Let $x$ be a set. Then the geometric fiber of $x$ is a point of the etale topology.

the small etale pretopology of X (from the name)

Let $X$ be a scheme. Then the small etale pretopology of $X$ is a pretopology of the set of etales of $X$ defined as the small pretopology of the proposition that $\operatorname{Etale}$ and the proposition that $\operatorname{Etale}$.

the small etale topology of X (from the name)

Let $X$ be a scheme. Then the small etale topology of $X$ is a Grothendieck topology of the set of etales of $X$ defined as the small Grothendieck topology of the proposition that $\operatorname{Etale}$ and $X$.

the point small etale of s (from the name)

Let $s$ be a homomorphism of the spectrum of $\operatorname{of}$ applied to $x$ and $S$. Then the point small etale of $s$ is a point of the small etale topology of $S$.

the point small etale fiber object to preimage of s and t (from the name)

Let $s$ be a homomorphism of the spectrum of $\operatorname{of}$ applied to $x$ and $S$ such that $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $s$ and $\operatorname{default}$ is equal to $x_{2}$. Let $t$ be an element of the action of the fiber of the point small etale of $s$ and $X$. Then the point small etale fiber object to preimage of $s$ and $t$ is an element of the preimage of $\operatorname{coe}$ applied to the homomorphism of the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the homomorphism of $\operatorname{toComma}$ applied to $X$ and $\operatorname{singleton}$ applied to $x_{2}$ defined as $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to the left of $t$ and $\operatorname{default}$.

$\operatorname{fppfPrecoverage}$ is a precoverage of the set of schemes defined as the precoverage of the minimum of the proposition that $\operatorname{Flat}$ and $\operatorname{LocallyOfFinitePresentation}$.

$\operatorname{fppfTopology}$ is a Grothendieck topology of the set of schemes defined as $\operatorname{toGrothendieck}$ applied to $\operatorname{fppfPrecoverage}$.

$\operatorname{fpqcPrecoverage}$ is a precoverage of the set of schemes defined as $\operatorname{propQCPrecoverage}$ applied to the proposition that $\operatorname{Flat}$.

$\operatorname{fpqcTopology}$ is a Grothendieck topology of the set of schemes defined as $\operatorname{toGrothendieck}$ applied to $\operatorname{fpqcPrecoverage}$.

P is a jointly surjective preserving (from the name)

the jointly surjective precoverage (from the name)

the precoverage of P (from the name)

the Zariski precoverage (from the name)

The Zariski precoverage is a precoverage of the set of schemes defined as the precoverage of $\operatorname{IsOpenImmersion}$.

the Grothendieck topology of P (from the name)

Let $P$ be a morphism property of the set of schemes. Then the Grothendieck topology of $P$ is a Grothendieck topology of the set of schemes defined as $\operatorname{toGrothendieck}$ applied to the precoverage of $P$.

the jointly surjective pretopology (from the name)

the jointly surjective topology (from the name)

the pretopology of P (from the name)

Let $P$ be a morphism property of the set of schemes. Then the pretopology of $P$ is a pretopology of the set of schemes defined as the pretopology of the set of schemes and the precoverage of $P$.

Let $S$ be a scheme. Then an element of $\operatorname{ProEt}$ applied to $S$ is an element of the function that maps $S$ to $\operatorname{Over}$ applied to $\operatorname{WeaklyEtale}$, the top and $S$.

the equivalence of S (from the name)

Let $S$ be a scheme. Then the equivalence of $S$ is an equivalence of $\operatorname{ProEt}$ applied to $S$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ defined as $\operatorname{overEquivOfIsInitial}$ applied to $\operatorname{WeaklyEtale}$, the top, $S$ and $\operatorname{isInitialOfIsEmpty}$.

Let $S$ be a scheme. Then $\operatorname{forget}$ applied to $S$ is a functor of $\operatorname{ProEt}$ applied to $S$ and $\operatorname{Over}$ applied to $S$ defined as the forgetful functor from the full subcategory of $\operatorname{WeaklyEtale}$.

Let $S$ be a scheme. Then $\operatorname{forgetFullyFaithful}$ applied to $S$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{forget}$ applied to $S$ defined as the forgetful functor from the full subcategory of the identity of the set of schemes.

Let $f$ be a homomorphism of $X$ and $S$. Then $\operatorname{mk}$ applied to $f$ is an element of $\operatorname{ProEt}$ applied to $S$ defined as $\operatorname{mk}$ applied to the top, $f$ and $h$.

the precoverage of S (from the name)

Let $S$ be a scheme. Then the precoverage of $S$ is a precoverage of $\operatorname{ProEt}$ applied to $S$ defined as the preimage of the composition of $\operatorname{forget}$ applied to $S$ and $\operatorname{forget}$ applied to $S$ and $\operatorname{proetalePrecoverage}$.

the topology of S (from the name)

Let $S$ be a scheme. Then the topology of $S$ is a Grothendieck topology of $\operatorname{ProEt}$ applied to $S$ defined as $\operatorname{toGrothendieck}$ applied to the precoverage of $S$.

$\operatorname{proetalePrecoverage}$ is a precoverage of the set of schemes defined as $\operatorname{propQCPrecoverage}$ applied to $\operatorname{WeaklyEtale}$.

$\operatorname{proetaleTopology}$ is a Grothendieck topology of the set of schemes defined as $\operatorname{toGrothendieck}$ applied to $\operatorname{proetalePrecoverage}$.

Let $x$ be a cover of $\operatorname{propQCPrecoverage}$ applied to $P$ and $S$. Then $\operatorname{forgetQc}$ applied to $x$ is a cover of the precoverage of $P$ and $S$.

the cover of x (from the name)

Let $x$ be a cover of the precoverage of $P$ and $S$. Then the cover of $x$ is a cover of $\operatorname{propQCPrecoverage}$ applied to $P$ and $S$.

Let $x$ be a cover of the precoverage of $P$ and $S$. Then $\operatorname{qculift}$ applied to $x$ is a cover of the precoverage of $P$ and $S$.

Let $P$ be a morphism property of the set of schemes. Then $\operatorname{propQCPrecoverage}$ applied to $P$ is a precoverage of the set of schemes defined as the minimum of $\operatorname{qcPrecoverage}$ and the precoverage of $P$.

Let $P$ be a morphism property of the set of schemes. Then $\operatorname{propQCTopology}$ applied to $P$ is a Grothendieck topology of the set of schemes defined as $\operatorname{toGrothendieck}$ applied to $\operatorname{propQCPrecoverage}$ applied to $P$.

$\operatorname{qcCoverFamily}$ is a zero hypercover family of the set of schemes.

$\operatorname{qcPrecoverage}$ is a precoverage of the set of schemes defined as the precoverage of $\operatorname{qcCoverFamily}$.

the glue data of hf (from the name)

Assume that for all elements $i$ of $x$, $\operatorname{presheaf}$ holds for $\operatorname{IsOpenImmersion}$. Then the glue data of $\mathrm{hf}$ is a glue data.

Assume that for all elements $i$ of $x$, $\operatorname{presheaf}$ holds for $\operatorname{IsOpenImmersion}$. Then $\operatorname{representableBy}$ applied to $\mathrm{hf}$ is an element of $\operatorname{RepresentableBy}$ applied to the object of $F$ and the glued scheme of the glue data of $\mathrm{hf}$ defined as $\operatorname{symm}$ applied to $\operatorname{representableByEquiv}$ and the map isomorphism of the sheaf to presheaf of the Zariski topology and the set of sets and the Yoneda isomorphism sheaf of $\mathrm{hf}$.

Assume that for all elements $i_{1}$ of $x$, $\operatorname{presheaf}$ holds for $\operatorname{IsOpenImmersion}$. Let $i$ be an element of $x$. Then $\operatorname{toGlued}$ applied to $\mathrm{hf}$ and $i$ is a homomorphism of $X$ applied to $i$ and the glued scheme of the glue data of $\mathrm{hf}$ defined as the inclusion of the glue data of $\mathrm{hf}$ and $i$.

the map from the glued scheme of hf (from the docstring)

Assume that for all elements $i$ of $x$, $\operatorname{presheaf}$ holds for $\operatorname{IsOpenImmersion}$. Then the map from the glued scheme of $\mathrm{hf}$ is a homomorphism of the action of the Yoneda of the Zariski topology and the glued scheme of the glue data of $\mathrm{hf}$ and $F$.

the Yoneda isomorphism sheaf of hf (from the name)

Assume that for all elements $i$ of $x$, $\operatorname{presheaf}$ holds for $\operatorname{IsOpenImmersion}$. Then the Yoneda isomorphism sheaf of $\mathrm{hf}$ is an isomorphism of the action of the Yoneda of the Zariski topology and the glued scheme of the glue data of $\mathrm{hf}$ and $F$ defined as $\operatorname{asIso}$ applied to the map from the glued scheme of $\mathrm{hf}$.

Let $x$ be a cover of the precoverage of $P$ and the left of $X$. Then there is a presieve of $X$. Proof. Let $x$ be arbitrary. Let $i$ be arbitrary. By x. By CategoryTheory__Precoverage__ZeroHypercover__toPreZeroHypercover. By i. By CategoryTheory__PreZeroHypercover__X. By S. By AlgebraicGeometry__Scheme__asOver. Let $i_{1}$ be arbitrary. By x. By CategoryTheory__Precoverage__ZeroHypercover__toPreZeroHypercover. By i1. By CategoryTheory__PreZeroHypercover__f. By S. By AlgebraicGeometry__Scheme__Hom__asOver. By CategoryTheory__Presieve__ofArrows.

Let $x$ be a cover of the precoverage of $P$ and the left subobject of $\operatorname{toComma}$ applied to $X$ such that for all elements $j$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$, $Q$ holds for $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $j$, $S$ and $\operatorname{over}$ applied to $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x$ and $j$, $S$ and $\mathrm{inferInstance}$. Then there is a presieve of $X$. Proof. Let $x$ be arbitrary. Let $h_{1}$ be arbitrary. Let $i$ be arbitrary. By x. By CategoryTheory__Precoverage__ZeroHypercover__toPreZeroHypercover. By i. By CategoryTheory__PreZeroHypercover__X. By S. By i. By h1. By AlgebraicGeometry__Scheme__asOverProp. Let $i_{1}$ be arbitrary. By x. By CategoryTheory__Precoverage__ZeroHypercover__toPreZeroHypercover. By i1. By CategoryTheory__PreZeroHypercover__f. By S. By AlgebraicGeometry__Scheme__Hom__asOverProp. By CategoryTheory__Presieve__ofArrows.

Let $P$ be a morphism property of the set of schemes. Let $S$ be a scheme. Then $\operatorname{overGrothendieckTopology}$ applied to $P$ and $S$ is a Grothendieck topology of $\operatorname{Over}$ applied to $S$ defined as $\operatorname{over}$ applied to the Grothendieck topology of $P$ and $S$.

Let $P$ be a morphism property of the set of schemes. Let $S$ be a scheme. Then $\operatorname{overPretopology}$ applied to $P$ and $S$ is a pretopology of $\operatorname{Over}$ applied to $S$ defined as the pretopology of $\operatorname{Over}$ applied to $S$ and $\operatorname{over}$ applied to $S$ and the precoverage of $P$.

the small Grothendieck topology of P and S (from the name)

Let $P$ be a morphism property of the set of schemes. Let $S$ be a scheme. Then the small Grothendieck topology of $P$ and $S$ is a Grothendieck topology of $\operatorname{Over}$ applied to $Q$, the top and $S$ defined as the restricted topology of the forgetful functor from the full subcategory of $Q$ and $\operatorname{overGrothendieckTopology}$ applied to $P$ and $S$.

the small pretopology of P and Q (from the name)

Let $P$ and $Q$ be morphism properties of the set of schemes. Then the small pretopology of $P$ and $Q$ is a pretopology of $\operatorname{Over}$ applied to $Q$, the top and $S$ defined as the pretopology of $\operatorname{Over}$ applied to $Q$, the top and $S$ and the preimage of the forgetful functor from the full subcategory of $Q$ and $\operatorname{over}$ applied to $S$ and the precoverage of $P$.

Let $X$ be a scheme. Then an element of $\operatorname{AffineZariskiSite}$ applied to $X$ is an element of the function that maps $X$ to $\SubtypeSet {U}{\operatorname{IsAffineOpen} (U)}$.

Let $U$ be an element of $\operatorname{AffineZariskiSite}$ applied to $X$. Let $f$ be a carrier of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the open of $U$. Then $\operatorname{basicOpen}$ applied to $U$ and $f$ is an element of $\operatorname{AffineZariskiSite}$ applied to $X$ defined as $\operatorname{basicOpen}$ applied to $X$ and $f$.

the cocone of X (from the name)

Let $X$ be a scheme. Then the cocone of $X$ is a cocone of the composition of the open functor of $X$ and the composition of the right opposite of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and the spectrum.

the directed cover of X (from the docstring)

Let $X$ be a scheme. Then the directed cover of $X$ is an open cover of $X$.

the Grothendieck topology of X (from the name)

Let $X$ be a scheme. Then the Grothendieck topology of $X$ is a Grothendieck topology of $\operatorname{AffineZariskiSite}$ applied to $X$ defined as the induced topology of the open functor of $X$ and the Grothendieck topology of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$.

Let $X$ be a scheme. Then $\operatorname{isColimitCocone}$ applied to $X$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $X$.

the presieve of U and s (from the name)

Let $U$ be an element of $\operatorname{AffineZariskiSite}$ applied to $X$. Let $s$ be an element of the power set of the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the open of $U$. Then the presieve of $U$ and $s$ is a presieve of $U$ defined as the function that maps $V$ and $x$ to the proposition that there exists a carrier $f$ of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the open of $U$, such that $f$ is an element of $s$ and $\operatorname{basicOpen}$ applied to $X$ and $f$ is equal to the open of $V$.

the relative gluing data of H (from the name)

Assume that $\operatorname{Coequifibered}$ holds for the composition of the opposite of the open functor of $X$ and the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$, $F$ and $x$. Then the relative gluing data of $H$ is a relative gluing data of the directed cover of $X$.

Let $X$ be a scheme. Then $\operatorname{restrictIsoSpec}$ applied to $X$ is an isomorphism of the composition of the open functor of $X$ and the composition of $\operatorname{restrictFunctor}$ applied to $X$ and $\operatorname{forget}$ applied to $X$ and the composition of the open functor of $X$ and the composition of the right opposite of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and the spectrum.

the section of P (from the name)

Let $P$ be a presieve of $U$. Then the section of $P$ is an element of the power set of the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{op}$ applied to the open of $U$ defined as $\operatorname{ofPred}$ applied to the function that maps $f$ to $P$ applied to $\operatorname{basicOpen}$ applied to $U$ and $f$ and the homomorphism of $\mathrm{AlgebraicGeometry\_\_Scheme\_\_AffineZariskiSite\_\_basicOpen\_le}$ applied to $U$ and $f$.

the sheaf equivalence (from the name)

The sheaf equivalence is an equivalence of the set of sheaves of the Grothendieck topology of $X$ and $A$ and the set of sheaves of $A$ and the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ defined as the sheaf induced topology equivalence of the open functor of $X$ and the Grothendieck topology of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$.

the open of U (from the name)

Let $U$ be an element of $\operatorname{AffineZariskiSite}$ applied to $X$. Then the open of $U$ is an open of $X$ defined as $U$.

the open functor of X (from the name)

Let $X$ be a scheme. Then the open functor of $X$ is a functor of $\operatorname{AffineZariskiSite}$ applied to $X$ and the set of opens of $X$ defined as the functor of $\mathrm{AlgebraicGeometry\_\_Scheme\_\_AffineZariskiSite\_\_toOpens\_mono}$.

the spectrum identity (from the name)

the induced map of f (from the docstring)

the locally ringed space object of R (from the name)

the induced map of f (from the docstring)

Let $f$ be a homomorphism of $R$ and $S$. Then the induced map of $f$ is a homomorphism of the sheafed space object of $S$ and the sheafed space object of $R$.

the sheafed space object of R (from the name)

Let $R$ be a category of commutative rings. Then the sheafed space object of $R$ is a sheafed space of the set of categories of commutative rings.

the locally ringed space (from the name)

the presheafed space (from the name)

The presheafed space is a functor of the set of opposites of the set of categories of commutative rings and the set of presheafed spaces of the set of categories of commutative rings defined as the composition of the sheafed space and $\operatorname{forgetToPresheafedSpace}$.

the sheafed space (from the name)

The sheafed space is a functor of the set of opposites of the set of categories of commutative rings and the set of sheafed spaces of the set of categories of commutative rings.

the top (from the name)

The top is a functor of the set of opposites of the set of categories of commutative rings and the set of topological categories.

the induced map of f (from the docstring)

Let $f$ be a homomorphism of $R$ and $S$. Then the induced map of $f$ is a homomorphism of the top object of $S$ and the top object of $R$.

the top object of R (from the name)

Let $R$ be a category of commutative rings. Then the top object of $R$ is a topological category defined as $\operatorname{of}$ applied to the set of prime spectra of the set of carriers of $R$.

the pushforward stalk of f and p (from the name)

Let $f$ be a homomorphism of $R$ and $S$. Let $p$ be a prime spectrum of the set of carriers of $R$. Then the pushforward stalk of $f$ and $p$ is a homomorphism of $S$ and the stalk of the action of the pushforward functor of the set of categories of commutative rings and the induced map of $f$ and the object of the structure sheaf of the set of carriers of $S$ and $p$ defined as the composition of the commutative ring category of the algebra map of the set of carriers of $S$ and the action of the object of the structure sheaf in type of the set of carriers of $S$ and the set of carriers of $S$ and the action of the opposite of the map of the induced map of $f$ and $\operatorname{op}$ applied to the top and the germ of the top and $p$.

the pushforward stalk algebra homomorphism of S and p (from the name)

Let $R$ and $S$ be categories of commutative rings. Let $p$ be a prime spectrum of the set of carriers of $R$. Then the pushforward stalk algebra homomorphism of $S$ and $p$ is an algebra homomorphism of the set of carriers of $S$ and the set of carriers of the stalk of the action of the pushforward functor of the set of categories of commutative rings and the induced map of the commutative ring category of the algebra map of the set of carriers of $R$ and the set of carriers of $S$ and the object of the structure sheaf of the set of carriers of $S$ and $p$.

the spectrum of R (from the name)

X is a germ injective (from the name)

Let $X$ be a scheme. Then $X$ is a germ injective, if for all carriers $x$ of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$, $\operatorname{IsGermInjectiveAt}$ holds for $X$ and $x$.

Let $X$ be a scheme. Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then we can say that $\operatorname{IsGermInjectiveAt}$ holds for $X$ and $x$.

Assume that $U$ is affine. Assume that $x$ is an element of $U$. Then $\operatorname{fromSpecStalk}$ applied to $\mathrm{hU}$ and $\mathrm{hxU}$ is a homomorphism of the spectrum of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $x$ and $X$ defined as the composition of the induced map of the germ of $U$ and $x$ and $\operatorname{fromSpec}$ applied to $\mathrm{hU}$.

Let $U$ be an open of $X$. Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ such that $x$ is an element of $U$. Then $\operatorname{fromSpecStalkOfMem}$ applied to $U$, $x$ and $\mathrm{hxU}$ is a homomorphism of the spectrum of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $x$ and the scheme of $U$ defined as the composition of the induced map of the inverse of the stalk map of the inclusion of $U$ and $x$ and $\operatorname{fromSpecStalk}$ applied to the scheme of $U$ and $x$.

Let $X$ be a scheme. Let $x$ be a carrier of the carrier of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$. Then $\operatorname{fromSpecStalk}$ applied to $X$ and $x$ is a homomorphism of the spectrum of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $x$ and $X$.

Let $f$ be a homomorphism of the spectrum of $R$ and $X$. Then $\operatorname{stalkClosedPointTo}$ applied to $f$ is a homomorphism of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to $X$ and $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $\operatorname{toLRSHom'}$ applied to $f$ and the closed point in the prime spectrum of the set of carriers of $R$ and $R$ defined as the composition of the stalk map of $f$ and the closed point in the prime spectrum of the set of carriers of $R$ and the homomorphism of the stalk closed point isomorphism of $R$.

the spectrum to equivalence of X and R (from the name)

Let $X$ be a scheme. Let $R$ be a category of commutative rings. Then the spectrum to equivalence of $X$ and $R$ is an element of $\EquivMACRoAE {\operatorname{Hom} (\operatorname{Spec} (R), X)}{\Sigma (\lambda x . \SubtypeSet {f}{\mathrm{IsLocalHom} (\operatorname{hom} (f))})}$.

the stalk closed point isomorphism of R (from the name)

Let $R$ be a category of commutative rings. Then the stalk closed point isomorphism of $R$ is an isomorphism of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $\operatorname{toLocallyRingedSpace}$ applied to the spectrum of $R$ and the closed point in the prime spectrum of the set of carriers of $R$ and $R$.

the top of R (from the name)

Let $R$ be a set. Then the top of $R$ is a topological category defined as $\operatorname{of}$ applied to the set of prime spectra of $R$.

the structure sheaf of R (from the name)

Let $R$ be a set. Then the structure sheaf of $R$ is a sheaf of the set of categories of commutative rings and the top of $R$.

f is a fraction (from the name)

Let $f$ be a function from elements $x_{3}$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {U}{x_{4}})}$ to localizations of $M$ and $x_{3}$. Then $x_{3}$ is a fraction, if there exists an element $r$ of $M$, such that there exists an element $s$ of $R$, such that for all elements $x_{3}$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {U}{x_{4}})}$, there exists an element $\mathrm{hs}$ of $\mathrm{not}$ applied to $\MembershipmemMACRoT {\operatorname{asIdeal} (x_{3})}{s}$, such that $\EqtMACRoH {x_{3} (x_{3})}{\operatorname{mk} (r , s)}$.

localization of M and P (from the name)

Let $M$ be a set. Let $P$ be a carrier of the top of $R$. Then a localization of $M$ and $P$ is an element of the function that maps $M$ and $P$ to the set of localized modules of the complement of $\operatorname{asIdeal}$ applied to $P$ and $M$.

the preimage function of f and y (from the name)

Let $f$ be a linear map of $M$ and $N$. Let $y$ be a carrier of the top of $S$. Then the preimage function of $f$ and $y$ is a linear map of the set of localizations of $M$ and the preimage of $x_{6}$ and $y$ and the set of localizations of $N$ and $y$.

the preimage of U and V (from the name)

Let $f$ be a ring homomorphism of $R$ and $S$. Let $U$ be an open of the set of carriers of the top of $R$. Let $V$ be an open of the set of carriers of the top of $S$ such that the carrier of $V$ is less than or equal to the preimage of $\operatorname{comap}$ applied to $f$ and the carrier of $U$. Then the preimage of $U$ and $V$ is a ring homomorphism of the set of carriers of the action of the object of the structure sheaf of $R$ and $\operatorname{op}$ applied to $U$ and the set of carriers of the action of the object of the structure sheaf of $S$ and $\operatorname{op}$ applied to $V$.

the preimage function of s and x8 (from the name)

Let $f$ be a linear map of $M$ and $N$. Let $U$ be an open of the set of carriers of the top of $R$. Let $V$ be an open of the set of carriers of the top of $S$ such that the carrier of $V$ is less than or equal to the preimage of $\operatorname{comap}$ applied to $x_{6}$ and the carrier of $U$. Let $s$ be a function from elements $x_{8}$ of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {U}{x_{9}})}$ to localizations of $M$ and $x_{8}$. Let $y$ be an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {V}{x_{7}})}$. Then the preimage function of $x_{8}$ and $s$ is a localization of $N$ and $y$ defined as the function that maps $y$ to $\operatorname{comapFun}$ applied to $f$, $s$, $x_{8}$ applied to the preimage of $x_{6}$ and $s$ and $y$.

the preimage of U and V (from the name)

Let $f$ be a linear map of $M$ and $N$. Let $U$ be an open of the set of carriers of the top of $R$. Let $V$ be an open of the set of carriers of the top of $S$ such that the carrier of $V$ is less than or equal to the preimage of $\operatorname{comap}$ applied to $x_{6}$ and the carrier of $U$. Then the preimage of $U$ and $V$ is a linear map of the action of the object of the structure sheaf in type of $R$ and $M$ and $\operatorname{op}$ applied to $U$ and the action of the object of the structure sheaf in type of $S$ and $N$ and $\operatorname{op}$ applied to $V$.

the commutative ring category stalk equivalence module stalk of R and x1 (from the name)

Let $R$ be a set. Let $x_{1}$ be a carrier of the top of $R$. Then the commutative ring category stalk equivalence module stalk of $R$ and $x_{1}$ is a linear equivalence of the set of carriers of the stalk of the presheaf of the structure sheaf of $R$ and $R$ and $x_{1}$ and the set of carriers of the stalk of the structure presheaf in commutative ring category of $R$ and $x_{1}$.

the constant of g and U (from the name)

Let $f$ be an element of $M$. Let $g$ be an element of $R$. Let $U$ be an open of the set of carriers of the top of $R$ such that $U \leq \operatorname{basicOpen} (g)$. Then the constant of $g$ and $U$ is an element of the action of the object of the structure sheaf in type of $R$ and $M$ and $\operatorname{op}$ applied to $U$ defined as the function that maps $x_{3}$ to $\operatorname{mk}$ applied to $f$ and $g$.

the global section isomorphism of R (from the name)

Let $R$ be a set. Then the global section isomorphism of $R$ is an isomorphism of $\operatorname{of}$ applied to $R$ and the action of the object of the structure sheaf of $R$ and $\operatorname{op}$ applied to the top defined as the commutative ring category isomorphism of the ring isomorphism of the algebra map of $R$ and the action of the object of the structure sheaf in type of $R$ and $R$ and $\operatorname{op}$ applied to the top and $\mathrm{AlgebraicGeometry\_\_StructureSheaf\_\_algebraMap\_obj\_top\_bijective}$.

Let $R$ and $M$ be sets. Then $\operatorname{isFractionPrelocal}$ applied to $R$ and $M$ is a prelocal predicate of the set of elements of $\operatorname{Localizations}$ applied to $M$.

Let $R$ and $M$ be sets. Then $\operatorname{isLocallyFraction}$ applied to $R$ and $M$ is a local predicate of the set of elements of $\operatorname{Localizations}$ applied to $M$ defined as the sheafification of $\operatorname{isFractionPrelocal}$ applied to $R$ and $M$.

the section subalgebra of A and U (from the name)

Let $A$ be a set. Let $U$ be an open of the set of carriers of the top of $R$. Then the section subalgebra of $A$ and $U$ is a subalgebra of $R$ and the set of functions from elements $x_{3}$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {U}{x_{4}})}$ to localizations of $A$ and $x_{3}$.

the section subalgebra submodule of M and U (from the name)

Let $M$ be a set. Let $U$ be an open of the set of carriers of the top of $R$. Then the section subalgebra submodule of $M$ and $U$ is a submodule of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{sectionsSubalgebra} (R , U)}{x_{3}})}$ and the set of functions from elements $x_{4}$ of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {U}{x_{5}})}$ to localizations of $M$ and $x_{4}$.

the section submodule of M and U (from the name)

Let $M$ be a set. Let $U$ be an open of the set of carriers of the top of $R$. Then the section submodule of $M$ and $U$ is a submodule of $R$ and the set of functions from elements $x_{3}$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {U}{x_{4}})}$ to localizations of $M$ and $x_{3}$.

the stalk isomorphism of R and x1 (from the name)

Let $R$ be a set. Let $x_{1}$ be a prime spectrum of $R$. Then the stalk isomorphism of $R$ and $x_{1}$ is an algebra isomorphism of $\operatorname{AtPrime}$ applied to $\operatorname{asIdeal}$ applied to $x_{1}$ and the set of carriers of the stalk of the structure presheaf in commutative ring category of $R$ and $x_{1}$ defined as the algebra isomorphism of the complement of $\operatorname{asIdeal}$ applied to $x_{1}$.

the open of U (from the name)

Let $R$ and $M$ be sets. Let $U$ be an open of the set of carriers of the top of $R$. Then the open of $U$ is a linear map of $M$ and the action of the object of the structure sheaf in type of $R$ and $M$ and $\operatorname{op}$ applied to $U$.

the stalk of R and x1 (from the name)

Let $R$ be a set. Let $x_{1}$ be a carrier of the top of $R$. Then the stalk of $R$ and $x_{1}$ is a homomorphism of $\operatorname{of}$ applied to $R$ and the stalk of the structure presheaf in commutative ring category of $R$ and $x_{1}$ defined as the composition of the commutative ring category of the algebra map of $R$ and the action of the object of the structure sheaf in type of $R$ and $R$ and $\operatorname{op}$ applied to the top and the germ of the top and $x_{1}$.

the stalk of x3 (from the name)

Let $R$ and $M$ be sets. Let $x_{3}$ be a carrier of the top of $R$. Then the stalk of $x_{3}$ is a linear map of $M$ and the set of carriers of the stalk of the presheaf of the structure sheaf of $R$ and $M$ and $x_{3}$.

the structure sheaf of R and M (from the docstring)

Let $R$ and $M$ be sets. Then the structure sheaf of $R$ and $M$ is a presheaf of module of the composition of the structure presheaf in commutative ring category of $R$ and the forgetful functor of the set of categories of commutative rings and the set of categories of rings.

Let $R$ be a set. Then $\operatorname{structurePresheafCompForget}$ applied to $R$ is an isomorphism of the composition of the structure presheaf in commutative ring category of $R$ and the forgetful functor of the set of categories of commutative rings and the object of the structure sheaf in type of $R$ and $R$.

the structure presheaf in commutative ring category of R (from the name)

Let $R$ be a set. Then the structure presheaf in commutative ring category of $R$ is a presheaf of the set of categories of commutative rings and the top of $R$.

the structure presheaf in module category of R and M (from the name)

Let $R$ and $M$ be sets. Then the structure presheaf in module category of $R$ and $M$ is a presheaf of the set of module categories of $R$ and the top of $R$.

the structure sheaf in type of R and M (from the name)

Let $R$ and $M$ be sets. Then the structure sheaf in type of $R$ and $M$ is a sheaf of the set of sets and the top of $R$ defined as the subsheaf to type of $\operatorname{isLocallyFraction}$ applied to $R$ and $M$.

valuative commutative square of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the valuative commutative squares of $f$ are a basic type.

Let $\mathrm{self}$ be a valuative commutative square of $f$. Then an element of $\operatorname{K}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj4}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a valuative commutative square of $f$. Then an element of $\operatorname{R}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a valuative commutative square of $f$. Then $\mathrm{AlgebraicGeometry\_\_ValuativeCommSq\_\_i\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of the spectrum of $\operatorname{of}$ applied to $\operatorname{K}$ applied to $\mathrm{self}$ and $X$ defined as $\operatorname{proj8}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a valuative commutative square of $f$. Then $\mathrm{AlgebraicGeometry\_\_ValuativeCommSq\_\_i\_u2082\_}$ applied to $\mathrm{self}$ is a homomorphism of the spectrum of $\operatorname{of}$ applied to $\operatorname{R}$ applied to $\mathrm{self}$ and $Y$ defined as $\operatorname{proj9}$ applied to $\mathrm{self}$.

the valuative criterion (from the name)

The valuative criterion is a morphism property of the set of schemes defined as the function that maps $x$, $x_{1}$ and $f$ to the proposition that for all valuative commutative squares $S$ of $f$, $\mathrm{Nonempty}$ holds for the proposition that $\operatorname{LiftStruct}$ applied to $\operatorname{commSq}$ applied to $S$ is unique.

the existence (from the name)

The existence is a morphism property of the set of schemes defined as the function that maps $x$, $x_{1}$ and $f$ to the proposition that for all valuative commutative squares $S$ of $f$, $\operatorname{commSq}$ applied to $S$ has lifts.

the uniqueness (from the name)

The uniqueness is a morphism property of the set of schemes defined as the function that maps $x$, $x_{1}$ and $f$ to the proposition that for all valuative commutative squares $S$ of $f$, $\operatorname{LiftStruct}$ applied to $\operatorname{commSq}$ applied to $S$ is a subsingleton.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{quasiFiniteLocus}$ applied to $f$ is an open of $X$ defined as $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $x$ to $\operatorname{QuasiFiniteAt}$ applied to $f$ and $x$ and $\mathrm{AlgebraicGeometry\_\_Scheme\_\_Hom\_\_isOpen\_quasiFiniteAt}$ applied to $f$.