Loogle!
Result
Found 180 declarations mentioning AlgebraicGeometry.Spec.map.
- AlgebraicGeometry.Spec.map 📋 Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} (f : R ⟶ S) : AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec R - AlgebraicGeometry.instIsIsoSchemeMapOfCommRingCat 📋 Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} (f : R ⟶ S) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (AlgebraicGeometry.Spec.map f) - AlgebraicGeometry.Spec.map_id 📋 Mathlib.AlgebraicGeometry.Scheme
(R : CommRingCat) : AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R) - AlgebraicGeometry.Spec.map_eqToHom 📋 Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} (e : R = S) : AlgebraicGeometry.Spec.map (CategoryTheory.eqToHom e) = CategoryTheory.eqToHom ⋯ - AlgebraicGeometry.Spec.map_inv 📋 Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} (f : R ⟶ S) [CategoryTheory.IsIso f] : AlgebraicGeometry.Spec.map (CategoryTheory.inv f) = CategoryTheory.inv (AlgebraicGeometry.Spec.map f) - AlgebraicGeometry.Spec.map_comp 📋 Mathlib.AlgebraicGeometry.Scheme
{R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) : AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map g) (AlgebraicGeometry.Spec.map f) - AlgebraicGeometry.Scheme.Spec_map 📋 Mathlib.AlgebraicGeometry.Scheme
{X✝ Y✝ : CommRingCatᵒᵖ} (f : X✝ ⟶ Y✝) : AlgebraicGeometry.Scheme.Spec.map f = AlgebraicGeometry.Spec.map f.unop - AlgebraicGeometry.Spec.map_comp_assoc 📋 Mathlib.AlgebraicGeometry.Scheme
{R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec R ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map g) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) h) - AlgebraicGeometry.Spec.map_base 📋 Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} (f : R ⟶ S) : (AlgebraicGeometry.Spec.map f).base = TopCat.ofHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) - AlgebraicGeometry.Spec.map_base_apply 📋 Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} (f : R ⟶ S) (x : ↑↑(AlgebraicGeometry.Spec S).toPresheafedSpace) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Spec.map f).base) x = (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) x - AlgebraicGeometry.Spec_closedPoint 📋 Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} [IsLocalRing ↑R] [IsLocalRing ↑S] {f : R ⟶ S} [IsLocalHom (CommRingCat.Hom.hom f)] : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Spec.map f).base) (IsLocalRing.closedPoint ↑S) = IsLocalRing.closedPoint ↑R - AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality 📋 Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.Scheme.ΓSpecIso S).inv = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map f)) - AlgebraicGeometry.Scheme.ΓSpecIso_naturality 📋 Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map f)) (AlgebraicGeometry.Scheme.ΓSpecIso S).hom = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).hom f - AlgebraicGeometry.Spec.map_appLE 📋 Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} (f : R ⟶ S) {U : (AlgebraicGeometry.Spec S).Opens} {V : (AlgebraicGeometry.Spec R).Opens} (e : U ≤ (TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.map f).base).obj V) : AlgebraicGeometry.Scheme.Hom.appLE (AlgebraicGeometry.Spec.map f) V U e = CommRingCat.ofHom (AlgebraicGeometry.StructureSheaf.comap (CommRingCat.Hom.hom f) V U e) - AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc 📋 Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} (f : R ⟶ S) {Z : CommRingCat} (h : (AlgebraicGeometry.Spec S).presheaf.obj (Opposite.op ⊤) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso S).inv h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map f)) h) - AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc 📋 Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} (f : R ⟶ S) {Z : CommRingCat} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map f)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso S).hom h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).hom (CategoryTheory.CategoryStruct.comp f h) - AlgebraicGeometry.Spec.map_app 📋 Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} (f : R ⟶ S) (U : (AlgebraicGeometry.Spec R).Opens) : AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Spec.map f) U = CommRingCat.ofHom (AlgebraicGeometry.StructureSheaf.comap (CommRingCat.Hom.hom f) U ((TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.map f).base).obj U) ⋯) - AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom 📋 Mathlib.AlgebraicGeometry.Scheme
{X : AlgebraicGeometry.Scheme} {U V : X.Opens} (h : U = V) (W : (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op V))).Opens) : AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.eqToHom h).op)) W = CategoryTheory.eqToHom ⋯ - AlgebraicGeometry.IsOpenImmersion.of_isLocalization 📋 Mathlib.AlgebraicGeometry.OpenImmersion
{R S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] (f : R) [IsLocalization.Away f S] : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) - AlgebraicGeometry.Scheme.instIsOpenImmersionMapOfHomAwayAlgebraMap 📋 Mathlib.AlgebraicGeometry.OpenImmersion
{R : Type u_1} [CommRing R] (f : R) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f)))) - AlgebraicGeometry.Scheme.basic_open_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.OpenImmersion
{R : CommRingCat} (f : ↑R) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))) - AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_map 📋 Mathlib.AlgebraicGeometry.Cover.Open
{R : CommRingCat} {ι : Type u_1} (s : ι → ↑R) (hs : Ideal.span (Set.range s) = ⊤) (i : ι) : (AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop s hs).map i = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (s i)))) - AlgebraicGeometry.Spec.map_injective 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
{R S : CommRingCat} : Function.Injective AlgebraicGeometry.Spec.map - AlgebraicGeometry.Spec.map_surjective 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
{R S : CommRingCat} : Function.Surjective AlgebraicGeometry.Spec.map - AlgebraicGeometry.Spec.preimage_map 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
{R S : CommRingCat} (φ : R ⟶ S) : AlgebraicGeometry.Spec.preimage (AlgebraicGeometry.Spec.map φ) = φ - AlgebraicGeometry.Spec.map_preimage 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
{R S : CommRingCat} (f : AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec R) : AlgebraicGeometry.Spec.map (AlgebraicGeometry.Spec.preimage f) = f - AlgebraicGeometry.Spec.map_eq_id 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
{R : CommRingCat} {ϕ : R ⟶ R} : AlgebraicGeometry.Spec.map ϕ = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R) ↔ ϕ = CategoryTheory.CategoryStruct.id R - AlgebraicGeometry.Spec.map_inj 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
{R S : CommRingCat} {φ ψ : R ⟶ S} : AlgebraicGeometry.Spec.map φ = AlgebraicGeometry.Spec.map ψ ↔ φ = ψ - AlgebraicGeometry.Spec.homEquiv_symm_apply 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
{R S : CommRingCat} (f : R ⟶ S) : AlgebraicGeometry.Spec.homEquiv.symm f = AlgebraicGeometry.Spec.map f - AlgebraicGeometry.SpecMap_ΓSpecIso_hom 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
(R : CommRingCat) : AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.ΓSpecIso R).hom = (AlgebraicGeometry.Spec R).toSpecΓ - AlgebraicGeometry.Scheme.toSpecΓ_naturality 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f Y.toSpecΓ = CategoryTheory.CategoryStruct.comp X.toSpecΓ (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f)) - AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (Y.presheaf.obj (Opposite.op ⊤)) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp Y.toSpecΓ h) = CategoryTheory.CategoryStruct.comp X.toSpecΓ (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f)) h) - AlgebraicGeometry.Scheme.toSpecΓ_base 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
(X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : (CategoryTheory.ConcreteCategory.hom X.toSpecΓ.base) x = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Spec.map (X.presheaf.germ ⊤ x trivial)).base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) - AlgebraicGeometry.ΓSpecIso_obj_hom 📋 Mathlib.AlgebraicGeometry.GammaSpecAdjunction
{X : AlgebraicGeometry.Scheme} (U : X.Opens) : (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).hom = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map U.topIso.inv)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop (↑U).toSpecΓ) U.topIso.hom) - AlgebraicGeometry.specTargetImageFactorization_comp 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X ⟶ AlgebraicGeometry.Spec A) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.specTargetImageFactorization f) (AlgebraicGeometry.Spec.map (AlgebraicGeometry.specTargetImageRingHom f)) = f - AlgebraicGeometry.specTargetImageFactorization_comp_assoc 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X ⟶ AlgebraicGeometry.Spec A) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec A ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.specTargetImageFactorization f) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.specTargetImageRingHom f)) h) = CategoryTheory.CategoryStruct.comp f h - AlgebraicGeometry.arrowIsoΓSpecOfIsAffine 📋 Mathlib.AlgebraicGeometry.AffineScheme
{A B : CommRingCat} (f : A ⟶ B) : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map f)) - AlgebraicGeometry.arrowIsoSpecΓOfIsAffine 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f)) - AlgebraicGeometry.SpecMapRestrictBasicOpenIso 📋 Mathlib.AlgebraicGeometry.AffineScheme
{R S : CommRingCat} (f : R ⟶ S) (r : ↑R) : CategoryTheory.Arrow.mk (AlgebraicGeometry.Spec.map f ∣_ PrimeSpectrum.basicOpen r) ≅ CategoryTheory.Arrow.mk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r))) - AlgebraicGeometry.Scheme.isoSpec_Spec_hom 📋 Mathlib.AlgebraicGeometry.AffineScheme
(R : CommRingCat) : (AlgebraicGeometry.Spec R).isoSpec.hom = AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.ΓSpecIso R).hom - AlgebraicGeometry.Scheme.isoSpec_Spec_inv 📋 Mathlib.AlgebraicGeometry.AffineScheme
(R : CommRingCat) : (AlgebraicGeometry.Spec R).isoSpec.inv = AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.ΓSpecIso R).inv - AlgebraicGeometry.IsAffineOpen.map_fromSpec 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {V : X.Opens} (hV : AlgebraicGeometry.IsAffineOpen V) (f : Opposite.op U ⟶ Opposite.op V) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.map f)) hU.fromSpec = hV.fromSpec - AlgebraicGeometry.Scheme.arrowStalkMapSpecIso 📋 Mathlib.AlgebraicGeometry.AffineScheme
{R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) : CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap (AlgebraicGeometry.Spec.map f) p) ≅ CategoryTheory.Arrow.mk (CommRingCat.ofHom (Localization.localRingHom ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p).asIdeal p.asIdeal (CommRingCat.Hom.hom f) ⋯)) - AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_map 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} (U V : X.Opens) (h : U ≤ V) : CategoryTheory.CategoryStruct.comp U.toSpecΓ (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.homOfLE h).op)) = CategoryTheory.CategoryStruct.comp (X.homOfLE h) V.toSpecΓ - AlgebraicGeometry.Scheme.Opens.toSpecΓ.eq_1 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} (U : X.Opens) : U.toSpecΓ = CategoryTheory.CategoryStruct.comp (↑U).toSpecΓ (AlgebraicGeometry.Spec.map U.topIso.inv) - AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {V : X.Opens} {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (hV : AlgebraicGeometry.IsAffineOpen V) (i : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appLE f U V i)) hU.fromSpec = CategoryTheory.CategoryStruct.comp hV.fromSpec f - AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {V : X.Opens} (hV : AlgebraicGeometry.IsAffineOpen V) (f : Opposite.op U ⟶ Opposite.op V) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.map f)) (CategoryTheory.CategoryStruct.comp hU.fromSpec h) = CategoryTheory.CategoryStruct.comp hV.fromSpec h - AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_map_assoc 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} (U V : X.Opens) (h : U ≤ V) {Z : AlgebraicGeometry.Scheme} (h✝ : AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op V)) ⟶ Z) : CategoryTheory.CategoryStruct.comp U.toSpecΓ (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.homOfLE h).op)) h✝) = CategoryTheory.CategoryStruct.comp (X.homOfLE h) (CategoryTheory.CategoryStruct.comp V.toSpecΓ h✝) - AlgebraicGeometry.Scheme.isoSpec_hom_naturality 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp X.isoSpec.hom (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f)) = CategoryTheory.CategoryStruct.comp f Y.isoSpec.hom - AlgebraicGeometry.Scheme.isoSpec_inv_naturality 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f)) Y.isoSpec.inv = CategoryTheory.CategoryStruct.comp X.isoSpec.inv f - AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec_assoc 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {V : X.Opens} {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (hV : AlgebraicGeometry.IsAffineOpen V) (i : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appLE f U V i)) (CategoryTheory.CategoryStruct.comp hU.fromSpec h) = CategoryTheory.CategoryStruct.comp hV.fromSpec (CategoryTheory.CategoryStruct.comp f h) - AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (Y.presheaf.obj (Opposite.op ⊤)) ⟶ Z) : CategoryTheory.CategoryStruct.comp X.isoSpec.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f)) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp Y.isoSpec.hom h) - AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f)) (CategoryTheory.CategoryStruct.comp Y.isoSpec.inv h) = CategoryTheory.CategoryStruct.comp X.isoSpec.inv (CategoryTheory.CategoryStruct.comp f h) - AlgebraicGeometry.affineTargetImageInclusion.eq_1 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : AlgebraicGeometry.affineTargetImageInclusion f = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.specTargetImageRingHom (CategoryTheory.CategoryStruct.comp f Y.isoSpec.hom))) Y.isoSpec.inv - AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso 📋 Mathlib.AlgebraicGeometry.AffineScheme
{R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.stalkIso (↑R) ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p)).hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (Localization.localRingHom ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p).asIdeal p.asIdeal (CommRingCat.Hom.hom f) ⋯)) (AlgebraicGeometry.StructureSheaf.stalkIso (↑S) p).inv) = AlgebraicGeometry.Scheme.Hom.stalkMap (AlgebraicGeometry.Spec.map f) p - AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↥U) : hU.primeIdealOf x = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Spec.map (X.presheaf.germ U ↑x ⋯)).base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk ↑x)) - AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↥U) : (CategoryTheory.ConcreteCategory.hom hU.isoSpec.hom.base) x = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Spec.map (X.presheaf.germ U ↑x ⋯)).base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk ↑x)) - AlgebraicGeometry.Scheme.Hom.liftQuotient_comp 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X.Hom (AlgebraicGeometry.Spec A)) (I : Ideal ↑A) (hI : I ≤ RingHom.ker (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso A).inv f.appTop))) : CategoryTheory.CategoryStruct.comp (f.liftQuotient I hI) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = f - AlgebraicGeometry.Scheme.Hom.liftQuotient_comp_assoc 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X.Hom (AlgebraicGeometry.Spec A)) (I : Ideal ↑A) (hI : I ≤ RingHom.ker (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso A).inv f.appTop))) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of ↑A) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.liftQuotient I hI) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) h) = CategoryTheory.CategoryStruct.comp f h - AlgebraicGeometry.Scheme.Hom.liftQuotient.eq_1 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X.Hom (AlgebraicGeometry.Spec A)) (I : Ideal ↑A) (hI : I ≤ RingHom.ker (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso A).inv f.appTop))) : f.liftQuotient I hI = CategoryTheory.CategoryStruct.comp X.toSpecΓ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.lift I (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso A).inv f.appTop)) hI))) - AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply 📋 Mathlib.AlgebraicGeometry.AffineScheme
{R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) (x : CategoryTheory.ToType ((AlgebraicGeometry.Spec.structureSheaf ↑R).presheaf.stalk ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.StructureSheaf.localizationToStalk (↑S) p)) ((Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) ⋯) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom (↑R) ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p))) x)) = (AlgebraicGeometry.Scheme.Hom.stalkMap (AlgebraicGeometry.Spec.map f) p) x - AlgebraicGeometry.IsAffineOpen.isoSpec_inv 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) : hU.isoSpec.inv = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)) (↑U).isoSpec.inv - AlgebraicGeometry.isPullback_Spec_map_isPushout 📋 Mathlib.AlgebraicGeometry.Pullbacks
{A B C P : CommRingCat} (f : A ⟶ B) (g : A ⟶ C) (inl : B ⟶ P) (inr : C ⟶ P) (h : CategoryTheory.IsPushout f g inl inr) : CategoryTheory.IsPullback (AlgebraicGeometry.Spec.map inl) (AlgebraicGeometry.Spec.map inr) (AlgebraicGeometry.Spec.map f) (AlgebraicGeometry.Spec.map g) - AlgebraicGeometry.pullbackSpecIso 📋 Mathlib.AlgebraicGeometry.Pullbacks
(R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))) ≅ AlgebraicGeometry.Spec (CommRingCat.of (TensorProduct R S T)) - AlgebraicGeometry.isPullback_Spec_map_pushout 📋 Mathlib.AlgebraicGeometry.Pullbacks
{A B C : CommRingCat} (f : A ⟶ B) (g : A ⟶ C) : CategoryTheory.IsPullback (AlgebraicGeometry.Spec.map (CategoryTheory.Limits.pushout.inl f g)) (AlgebraicGeometry.Spec.map (CategoryTheory.Limits.pushout.inr f g)) (AlgebraicGeometry.Spec.map f) (AlgebraicGeometry.Spec.map g) - AlgebraicGeometry.pullbackSpecIso_inv_fst 📋 Mathlib.AlgebraicGeometry.Pullbacks
(R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).inv (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom) - AlgebraicGeometry.pullbackSpecIso_hom_fst 📋 Mathlib.AlgebraicGeometry.Pullbacks
(R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))) - AlgebraicGeometry.diagonal_Spec_map 📋 Mathlib.AlgebraicGeometry.Pullbacks
(R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : CategoryTheory.Limits.pullback.diagonal (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)) (AlgebraicGeometry.pullbackSpecIso R S S).inv - AlgebraicGeometry.pullbackSpecIso_inv_fst_assoc 📋 Mathlib.AlgebraicGeometry.Pullbacks
(R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) h - AlgebraicGeometry.pullbackSpecIso_hom_fst_assoc 📋 Mathlib.AlgebraicGeometry.Pullbacks
(R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))) h - AlgebraicGeometry.pullbackSpecIso_inv_snd 📋 Mathlib.AlgebraicGeometry.Pullbacks
(R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).inv (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight) - AlgebraicGeometry.pullbackSpecIso_hom_snd 📋 Mathlib.AlgebraicGeometry.Pullbacks
(R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)) = CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))) - AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc 📋 Mathlib.AlgebraicGeometry.Pullbacks
(R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of T) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)) h - AlgebraicGeometry.pullbackSpecIso_hom_snd_assoc 📋 Mathlib.AlgebraicGeometry.Pullbacks
(R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of T) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))) h - AlgebraicGeometry.instIsOpenImmersionMapOfHomForallEvalRingHom 📋 Mathlib.AlgebraicGeometry.Limits
{ι : Type u} (i : ι) (R : ι → Type (max u_1 u)) [(i : ι) → CommRing (R i)] : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x => R x) i))) - AlgebraicGeometry.coprodSpec_inl 📋 Mathlib.AlgebraicGeometry.Limits
(R S : Type u) [CommRing R] [CommRing S] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (AlgebraicGeometry.coprodSpec R S) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.fst R S)) - AlgebraicGeometry.coprodSpec_inr 📋 Mathlib.AlgebraicGeometry.Limits
(R S : Type u) [CommRing R] [CommRing S] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (AlgebraicGeometry.coprodSpec R S) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.snd R S)) - AlgebraicGeometry.coprodSpec.eq_1 📋 Mathlib.AlgebraicGeometry.Limits
(R S : Type u) [CommRing R] [CommRing S] : AlgebraicGeometry.coprodSpec R S = CategoryTheory.Limits.coprod.desc (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.fst R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.snd R S))) - AlgebraicGeometry.ι_sigmaSpec 📋 Mathlib.AlgebraicGeometry.Limits
{ι : Type u} (R : ι → CommRingCat) (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun i => AlgebraicGeometry.Spec (R i)) i) (AlgebraicGeometry.sigmaSpec R) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i => ↑(R i)) i)) - AlgebraicGeometry.coprodSpec_inl_assoc 📋 Mathlib.AlgebraicGeometry.Limits
(R S : Type u) [CommRing R] [CommRing S] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (R × S)) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.coprodSpec R S) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.fst R S))) h - AlgebraicGeometry.coprodSpec_inr_assoc 📋 Mathlib.AlgebraicGeometry.Limits
(R S : Type u) [CommRing R] [CommRing S] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (R × S)) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.coprodSpec R S) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.snd R S))) h - AlgebraicGeometry.ι_sigmaSpec_assoc 📋 Mathlib.AlgebraicGeometry.Limits
{ι : Type u} (R : ι → CommRingCat) (i : ι) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun i => AlgebraicGeometry.Spec (R i)) i) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.sigmaSpec R) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i => ↑(R i)) i))) h - AlgebraicGeometry.stalkwise_Spec_map_iff 📋 Mathlib.AlgebraicGeometry.Morphisms.Constructors
{P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) {R S : CommRingCat} (φ : R ⟶ S) : AlgebraicGeometry.stalkwise (fun {R S} [CommRing R] [CommRing S] => P) (AlgebraicGeometry.Spec.map φ) ↔ ∀ (p : Ideal ↑S) (x : p.IsPrime), P (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯) - AlgebraicGeometry.isOpenImmersion_SpecMap_iff_of_surjective 📋 Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
{R S : CommRingCat} (f : R ⟶ S) (hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map f) ↔ ∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e} - AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty_of_isLocalAtSource_of_isLocalAtTarget 📋 Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
(P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocalAtTarget P] [AlgebraicGeometry.IsLocalAtSource P] : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] f => P (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f)) - AlgebraicGeometry.HasRingHomProperty.of_isLocalAtSource_of_isLocalAtTarget 📋 Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
(P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocalAtTarget P] [AlgebraicGeometry.IsLocalAtSource P] : AlgebraicGeometry.HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] f => P (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f)) - AlgebraicGeometry.HasRingHomProperty.Spec_iff 📋 Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {R S : CommRingCat} {φ : R ⟶ S} : P (AlgebraicGeometry.Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ) - AlgebraicGeometry.SurjectiveOnStalks.Spec_iff 📋 Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
{R S : CommRingCat} {φ : R ⟶ S} : AlgebraicGeometry.SurjectiveOnStalks (AlgebraicGeometry.Spec.map φ) ↔ (CommRingCat.Hom.hom φ).SurjectiveOnStalks - AlgebraicGeometry.IsPreimmersion.of_isLocalization 📋 Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
{R S : Type u} [CommRing R] (M : Submonoid R) [CommRing S] [Algebra R S] [IsLocalization M S] : AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) - AlgebraicGeometry.IsPreimmersion.mk_Spec_map 📋 Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
{R S : CommRingCat} {f : R ⟶ S} (h₁ : Topology.IsEmbedding ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f))) (h₂ : (CommRingCat.Hom.hom f).SurjectiveOnStalks) : AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.Spec.map f) - AlgebraicGeometry.IsPreimmersion.Spec_map_iff 📋 Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
{R S : CommRingCat} (f : R ⟶ S) : AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.Spec.map f) ↔ Topology.IsEmbedding ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ (CommRingCat.Hom.hom f).SurjectiveOnStalks - AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι_ι 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
{X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))) (AlgebraicGeometry.IsAffineOpen.fromSpec ⋯) - AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι.eq_1 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
{X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : I.glueDataObjι U = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))) (AlgebraicGeometry.IsAffineOpen.isoSpec ⋯).inv - AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom.eq_1 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
{X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : ↑X.affineOpens) : AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom h U = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) - AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap.eq_1 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
{X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V) : I.glueDataObjMap h = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) ⋯)) - AlgebraicGeometry.Scheme.Spec_fromSpecStalk' 📋 Mathlib.AlgebraicGeometry.Stalk
(R : CommRingCat) (x : ↑↑(AlgebraicGeometry.Spec R).toPresheafedSpace) : (AlgebraicGeometry.Spec R).fromSpecStalk x = AlgebraicGeometry.Spec.map (AlgebraicGeometry.StructureSheaf.toStalk (↑R) x) - AlgebraicGeometry.Spec_stalkClosedPointIso 📋 Mathlib.AlgebraicGeometry.Stalk
(R : CommRingCat) [IsLocalRing ↑R] : AlgebraicGeometry.Spec.map (AlgebraicGeometry.stalkClosedPointIso R).inv = (AlgebraicGeometry.Spec R).fromSpecStalk (IsLocalRing.closedPoint ↑R) - AlgebraicGeometry.Scheme.instIsOverMapStalkSpecializesCommRingCatPresheaf 📋 Mathlib.AlgebraicGeometry.Stalk
{X : AlgebraicGeometry.Scheme} {x y : ↑↑X.toPresheafedSpace} (h : x ⤳ y) : AlgebraicGeometry.Scheme.Hom.IsOver (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes h)) X - AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk 📋 Mathlib.AlgebraicGeometry.Stalk
{X : AlgebraicGeometry.Scheme} {x y : ↑↑X.toPresheafedSpace} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes h)) (X.fromSpecStalk y) = X.fromSpecStalk x - AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk_assoc 📋 Mathlib.AlgebraicGeometry.Stalk
{X : AlgebraicGeometry.Scheme} {x y : ↑↑X.toPresheafedSpace} (h : x ⤳ y) {Z : AlgebraicGeometry.Scheme} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes h)) (CategoryTheory.CategoryStruct.comp (X.fromSpecStalk y) h✝) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) h✝ - AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk 📋 Mathlib.AlgebraicGeometry.Stalk
{X : AlgebraicGeometry.Scheme} {R : CommRingCat} [IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.stalkClosedPointTo f)) (X.fromSpecStalk ((CategoryTheory.ConcreteCategory.hom f.base) (IsLocalRing.closedPoint ↑R))) = f - AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass 📋 Mathlib.AlgebraicGeometry.Stalk
{X Y : AlgebraicGeometry.Scheme} [X.Over Y] {x : ↑↑X.toPresheafedSpace} : AlgebraicGeometry.Scheme.Hom.IsOver (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.stalkMap (X ↘ Y) x)) Y - AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk 📋 Mathlib.AlgebraicGeometry.Stalk
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {x : ↑↑X.toPresheafedSpace} : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.stalkMap f x)) (Y.fromSpecStalk ((CategoryTheory.ConcreteCategory.hom f.base) x)) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) f - AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem.eq_1 📋 Mathlib.AlgebraicGeometry.Stalk
{X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : ↑↑X.toPresheafedSpace) (hxU : x ∈ U) : U.fromSpecStalkOfMem x hxU = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CategoryTheory.inv (AlgebraicGeometry.Scheme.Hom.stalkMap U.ι ⟨x, hxU⟩))) ((↑U).fromSpecStalk ⟨x, hxU⟩) - AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc 📋 Mathlib.AlgebraicGeometry.Stalk
{X : AlgebraicGeometry.Scheme} {R : CommRingCat} [IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.stalkClosedPointTo f)) (CategoryTheory.CategoryStruct.comp (X.fromSpecStalk ((CategoryTheory.ConcreteCategory.hom f.base) (IsLocalRing.closedPoint ↑R))) h) = CategoryTheory.CategoryStruct.comp f h - AlgebraicGeometry.IsAffineOpen.fromSpecStalk.eq_1 📋 Mathlib.AlgebraicGeometry.Stalk
{X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {x : ↑↑X.toPresheafedSpace} (hxU : x ∈ U) : hU.fromSpecStalk hxU = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.germ U x hxU)) hU.fromSpec - AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk_assoc 📋 Mathlib.AlgebraicGeometry.Stalk
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {x : ↑↑X.toPresheafedSpace} {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.stalkMap f x)) (CategoryTheory.CategoryStruct.comp (Y.fromSpecStalk ((CategoryTheory.ConcreteCategory.hom f.base) x)) h) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) (CategoryTheory.CategoryStruct.comp f h) - AlgebraicGeometry.Scheme.Spec_fromSpecStalk 📋 Mathlib.AlgebraicGeometry.Stalk
(R : CommRingCat) (x : ↑↑(AlgebraicGeometry.Spec R).toPresheafedSpace) : (AlgebraicGeometry.Spec R).fromSpecStalk x = AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv ((AlgebraicGeometry.Spec R).presheaf.germ ⊤ x trivial)) - AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ 📋 Mathlib.AlgebraicGeometry.Stalk
{X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : ↑↑X.toPresheafedSpace) (hxU : x ∈ U) : CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) U.toSpecΓ = AlgebraicGeometry.Spec.map (X.presheaf.germ U x hxU) - AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ 📋 Mathlib.AlgebraicGeometry.Stalk
(X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) X.toSpecΓ = AlgebraicGeometry.Spec.map (X.presheaf.germ ⊤ x trivial) - AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc 📋 Mathlib.AlgebraicGeometry.Stalk
{X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : ↑↑X.toPresheafedSpace) (hxU : x ∈ U) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) (CategoryTheory.CategoryStruct.comp U.toSpecΓ h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.germ U x hxU)) h - AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc 📋 Mathlib.AlgebraicGeometry.Stalk
(X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op ⊤)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) (CategoryTheory.CategoryStruct.comp X.toSpecΓ h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.germ ⊤ x trivial)) h - AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec 📋 Mathlib.AlgebraicGeometry.Stalk
{R S : CommRingCat} [IsLocalRing ↑S] (φ : R ⟶ S) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).presheaf.germ ⊤ ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Spec.map φ).base) (IsLocalRing.closedPoint ↑S)) trivial) (AlgebraicGeometry.Scheme.stalkClosedPointTo (AlgebraicGeometry.Spec.map φ)) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).hom φ - AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk 📋 Mathlib.AlgebraicGeometry.Stalk
{X : AlgebraicGeometry.Scheme} {R : CommRingCat} [IsLocalRing ↑R] {x : ↑↑X.toPresheafedSpace} (f : X.presheaf.stalk x ⟶ R) [IsLocalHom (CommRingCat.Hom.hom f)] (U : X.Opens) (hU : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x)).base) (IsLocalRing.closedPoint ↑R) ∈ U) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x)).base) (IsLocalRing.closedPoint ↑R)) hU) (AlgebraicGeometry.Scheme.stalkClosedPointTo (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x))) = CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x ⋯) f - AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk_assoc 📋 Mathlib.AlgebraicGeometry.Stalk
{X : AlgebraicGeometry.Scheme} {R : CommRingCat} [IsLocalRing ↑R] {x : ↑↑X.toPresheafedSpace} (f : X.presheaf.stalk x ⟶ R) [IsLocalHom (CommRingCat.Hom.hom f)] (U : X.Opens) (hU : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x)).base) (IsLocalRing.closedPoint ↑R) ∈ U) {Z : CommRingCat} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x)).base) (IsLocalRing.closedPoint ↑R)) hU) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.stalkClosedPointTo (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x))) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x ⋯) (CategoryTheory.CategoryStruct.comp f h) - AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply 📋 Mathlib.AlgebraicGeometry.Stalk
(X : AlgebraicGeometry.Scheme) (R : CommRingCat) [IsLocalRing ↑R] (xf : (x : ↑↑X.toPresheafedSpace) × { f // IsLocalHom (CommRingCat.Hom.hom f) }) : (AlgebraicGeometry.SpecToEquivOfLocalRing X R).symm xf = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map ↑xf.snd) (X.fromSpecStalk xf.fst) - AlgebraicGeometry.Scheme.instIsPreimmersionMapResidue 📋 Mathlib.AlgebraicGeometry.ResidueField
{X : AlgebraicGeometry.Scheme} (x : ↑↑X.toPresheafedSpace) : AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.Spec.map (X.residue x)) - AlgebraicGeometry.Scheme.instIsOverMapHomCommRingCatResidueFieldCongr 📋 Mathlib.AlgebraicGeometry.ResidueField
{X : AlgebraicGeometry.Scheme} {x y : ↑↑X.toPresheafedSpace} (h : x = y) : AlgebraicGeometry.Scheme.Hom.IsOver (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.residueFieldCongr h).hom) X - AlgebraicGeometry.Scheme.residueFieldCongr_fromSpecResidueField 📋 Mathlib.AlgebraicGeometry.ResidueField
{X : AlgebraicGeometry.Scheme} {x y : ↑↑X.toPresheafedSpace} (h : x = y) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.residueFieldCongr h).hom) (X.fromSpecResidueField x) = X.fromSpecResidueField y - AlgebraicGeometry.Scheme.fromSpecResidueField.eq_1 📋 Mathlib.AlgebraicGeometry.ResidueField
(X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : X.fromSpecResidueField x = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.residue x)) (X.fromSpecStalk x) - AlgebraicGeometry.Scheme.residueFieldCongr_fromSpecResidueField_assoc 📋 Mathlib.AlgebraicGeometry.ResidueField
{X : AlgebraicGeometry.Scheme} {x y : ↑↑X.toPresheafedSpace} (h : x = y) {Z : AlgebraicGeometry.Scheme} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.residueFieldCongr h).hom) (CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) h✝) = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField y) h✝ - AlgebraicGeometry.Scheme.Spec_map_residue_apply 📋 Mathlib.AlgebraicGeometry.ResidueField
{X : AlgebraicGeometry.Scheme} (x : ↑↑X.toPresheafedSpace) (s : ↑↑(AlgebraicGeometry.Spec (X.residueField x)).toPresheafedSpace) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Spec.map (X.residue x)).base) s = IsLocalRing.closedPoint ↑(X.presheaf.stalk x) - AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField 📋 Mathlib.AlgebraicGeometry.ResidueField
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↑↑X.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)) (Y.fromSpecResidueField ((CategoryTheory.ConcreteCategory.hom f.base) x)) = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) f - AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass 📋 Mathlib.AlgebraicGeometry.ResidueField
{X Y : AlgebraicGeometry.Scheme} [X.Over Y] (x : ↑↑X.toPresheafedSpace) : AlgebraicGeometry.Scheme.Hom.IsOver (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap (X ↘ Y) x)) Y - AlgebraicGeometry.Scheme.descResidueField_fromSpecResidueField 📋 Mathlib.AlgebraicGeometry.ResidueField
{K : Type u_1} [Field K] (X : AlgebraicGeometry.Scheme) {x : ↑↑X.toPresheafedSpace} (f : X.presheaf.stalk x ⟶ CommRingCat.of K) [IsLocalHom (CommRingCat.Hom.hom f)] : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.descResidueField f)) (X.fromSpecResidueField x) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x) - AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc 📋 Mathlib.AlgebraicGeometry.ResidueField
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↑↑X.toPresheafedSpace) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)) (CategoryTheory.CategoryStruct.comp (Y.fromSpecResidueField ((CategoryTheory.ConcreteCategory.hom f.base) x)) h) = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) (CategoryTheory.CategoryStruct.comp f h) - AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField 📋 Mathlib.AlgebraicGeometry.ResidueField
(K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) (f : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.descResidueField (AlgebraicGeometry.Scheme.stalkClosedPointTo f))) (X.fromSpecResidueField ((CategoryTheory.ConcreteCategory.hom f.base) (IsLocalRing.closedPoint K))) = f - AlgebraicGeometry.IsClosedImmersion.Spec_map_residue 📋 Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
{X : AlgebraicGeometry.Scheme} (x : ↑↑X.toPresheafedSpace) : AlgebraicGeometry.IsClosedImmersion (AlgebraicGeometry.Spec.map (X.residue x)) - AlgebraicGeometry.IsClosedImmersion.spec_of_quotient_mk 📋 Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
{R : CommRingCat} (I : Ideal ↑R) : AlgebraicGeometry.IsClosedImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) - AlgebraicGeometry.IsClosedImmersion.spec_of_surjective 📋 Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
{R S : CommRingCat} (f : R ⟶ S) (h : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : AlgebraicGeometry.IsClosedImmersion (AlgebraicGeometry.Spec.map f) - AlgebraicGeometry.IsClosedImmersion.Spec_iff 📋 Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
{X : AlgebraicGeometry.Scheme} {R : CommRingCat} {f : X ⟶ AlgebraicGeometry.Spec R} : AlgebraicGeometry.IsClosedImmersion f ↔ ∃ I e, f = CategoryTheory.CategoryStruct.comp e.hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) - AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : CategoryTheory.CategoryStruct.comp T.SpecTensorTo (CategoryTheory.Limits.pullback.fst f g) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInl) (X.fromSpecResidueField T.x) - AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : CategoryTheory.CategoryStruct.comp T.SpecTensorTo (CategoryTheory.Limits.pullback.snd f g) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInr) (Y.fromSpecResidueField T.y) - AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {T T' : AlgebraicGeometry.Scheme.Pullback.Triplet f g} (h : T = T') : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr h).hom) T.SpecTensorTo = T'.SpecTensorTo - AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_map_tensorInl_fromSpecResidueField 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInl) (X.fromSpecResidueField T.x)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInr) (Y.fromSpecResidueField T.y)) g - AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.ofPointTensor t)) (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).SpecTensorTo = (CategoryTheory.Limits.pullback f g).fromSpecResidueField t - AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst_assoc 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp T.SpecTensorTo (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInl) (CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField T.x) h) - AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd_assoc 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp T.SpecTensorTo (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInr) (CategoryTheory.CategoryStruct.comp (Y.fromSpecResidueField T.y) h) - AlgebraicGeometry.Scheme.Pullback.Triplet.SpecTensorTo.eq_1 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : T.SpecTensorTo = CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInl) (X.fromSpecResidueField T.x)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInr) (Y.fromSpecResidueField T.y)) ⋯ - AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo_assoc 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {T T' : AlgebraicGeometry.Scheme.Pullback.Triplet f g} (h : T = T') {Z : AlgebraicGeometry.Scheme} (h✝ : CategoryTheory.Limits.pullback f g ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr h).hom) (CategoryTheory.CategoryStruct.comp T.SpecTensorTo h✝) = CategoryTheory.CategoryStruct.comp T'.SpecTensorTo h✝ - AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo_assoc 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) {Z : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback f g ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.ofPointTensor t)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).SpecTensorTo h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pullback f g).fromSpecResidueField t) h - AlgebraicGeometry.Scheme.Pullback.SpecOfPoint.eq_1 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) : AlgebraicGeometry.Scheme.Pullback.SpecOfPoint t = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.ofPointTensor t)).base) ⊥ - AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_map_tensor_isPullback 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : CategoryTheory.IsPullback (AlgebraicGeometry.Spec.map T.tensorInl) (AlgebraicGeometry.Spec.map T.tensorInr) (AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv (AlgebraicGeometry.Scheme.Hom.residueFieldMap f T.x))) (AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv (AlgebraicGeometry.Scheme.Hom.residueFieldMap g T.y))) - AlgebraicGeometry.Scheme.Pullback.carrierEquiv_eq_iff 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {T₁ T₂ : (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) × ↑↑(AlgebraicGeometry.Spec T.tensor).toPresheafedSpace} : T₁ = T₂ ↔ ∃ (e : T₁.fst = T₂.fst), (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e).inv).base) T₁.snd = T₂.snd - AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) (p : ↑↑(AlgebraicGeometry.Spec T.tensor).toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap T.SpecTensorTo p)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.ofPointTensor ((CategoryTheory.ConcreteCategory.hom T.SpecTensorTo.base) p))) (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯).hom)) = (AlgebraicGeometry.Spec T.tensor).fromSpecResidueField p - AlgebraicGeometry.IsIntegralHom.SpecMap_iff 📋 Mathlib.AlgebraicGeometry.Morphisms.Integral
{R S : CommRingCat} {φ : R ⟶ S} : AlgebraicGeometry.IsIntegralHom (AlgebraicGeometry.Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral - AlgebraicGeometry.AffineSpace.mapSpecMap 📋 Mathlib.AlgebraicGeometry.AffineSpace
{n : Type v} {R S : CommRingCat} (φ : R ⟶ S) : CategoryTheory.Arrow.mk (AlgebraicGeometry.AffineSpace.map n (AlgebraicGeometry.Spec.map φ)) ≅ CategoryTheory.Arrow.mk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) - AlgebraicGeometry.AffineSpace.SpecIso_inv_over 📋 Mathlib.AlgebraicGeometry.AffineSpace
{n : Type v} (R : CommRingCat) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.SpecIso n R).inv (AlgebraicGeometry.AffineSpace n (AlgebraicGeometry.Spec R) ↘ AlgebraicGeometry.Spec R) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom MvPolynomial.C) - AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc 📋 Mathlib.AlgebraicGeometry.AffineSpace
{n : Type v} (R : CommRingCat) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec R ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.SpecIso n R).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace n (AlgebraicGeometry.Spec R) ↘ AlgebraicGeometry.Spec R) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom MvPolynomial.C)) h - AlgebraicGeometry.AffineSpace.map_Spec_map 📋 Mathlib.AlgebraicGeometry.AffineSpace
{n : Type v} {R S : CommRingCat} (φ : R ⟶ S) : AlgebraicGeometry.AffineSpace.map n (AlgebraicGeometry.Spec.map φ) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.SpecIso n S).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) (AlgebraicGeometry.AffineSpace.SpecIso n R).inv) - AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply 📋 Mathlib.AlgebraicGeometry.AffineSpace
(n : Type v) {X : AlgebraicGeometry.Scheme} (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) : (AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n).symm v = CategoryTheory.CategoryStruct.comp X.toSpecΓ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (MvPolynomial.eval₂Hom ((algebraMap ℤ ↑(X.presheaf.toPrefunctor.1 (Opposite.op ⊤))).comp ULift.ringEquiv.toRingHom) v))) - AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over 📋 Mathlib.AlgebraicGeometry.AffineSpace
{n : Type v} (S : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine S] : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).inv (AlgebraicGeometry.AffineSpace n S ↘ S) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom MvPolynomial.C)) S.isoSpec.inv - AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc 📋 Mathlib.AlgebraicGeometry.AffineSpace
{n : Type v} (S : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine S] {Z : AlgebraicGeometry.Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace n S ↘ S) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom MvPolynomial.C)) (CategoryTheory.CategoryStruct.comp S.isoSpec.inv h) - AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom 📋 Mathlib.AlgebraicGeometry.AffineSpace
(n : Type v) (S : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine S] : (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).hom = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace n S).toSpecΓ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (MvPolynomial.eval₂Hom (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.AffineSpace n S ↘ S))) (AlgebraicGeometry.AffineSpace.coord S)))) - AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv 📋 Mathlib.AlgebraicGeometry.AffineSpace
(n : Type v) (S : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine S] : (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).inv = AlgebraicGeometry.AffineSpace.homOfVector (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom MvPolynomial.C)) S.isoSpec.inv) (⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑(S.presheaf.obj (Opposite.op ⊤))))).inv) ∘ MvPolynomial.X) - AlgebraicGeometry.IsSeparated.instMap 📋 Mathlib.AlgebraicGeometry.Morphisms.Separated
(R S : CommRingCat) (f : R ⟶ S) : AlgebraicGeometry.IsSeparated (AlgebraicGeometry.Spec.map f) - Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul 📋 Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
{R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FormallyUnramified R S] [Algebra.EssFiniteType R S] : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)) - AlgebraicGeometry.pointsPi.eq_1 📋 Mathlib.AlgebraicGeometry.PointsPi
{ι : Type u} (R : ι → CommRingCat) (X : AlgebraicGeometry.Scheme) (f : AlgebraicGeometry.Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X) (i : ι) : AlgebraicGeometry.pointsPi R X f i = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x => ↑(R x)) i))) f - AlgebraicGeometry.eq_bot_of_comp_quotientMk_eq_sigmaSpec 📋 Mathlib.AlgebraicGeometry.PointsPi
{ι : Type u} (R : ι → CommRingCat) (I : Ideal ((i : ι) → ↑(R i))) (f : (∐ fun i => AlgebraicGeometry.Spec (R i)) ⟶ AlgebraicGeometry.Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))) (hf : CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = AlgebraicGeometry.sigmaSpec R) : I = ⊥ - AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 x) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Proj 𝒜).homOfLE ⋯) (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 f) - AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap_assoc 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A} (hx : x = f * g) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 x) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) h) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Proj 𝒜).homOfLE ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 f) h) - AlgebraicGeometry.Proj.SpecMap_awayMap_awayι 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) = AlgebraicGeometry.Proj.awayι 𝒜 x ⋯ ⋯ - AlgebraicGeometry.Proj.SpecMap_awayMap_awayι_assoc 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A} (hx : x = f * g) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj 𝒜 ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 x ⋯ ⋯) h - AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx)) - AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯)) - AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm') - AlgebraicGeometry.Proj.basicOpenToSpec.eq_1 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) : AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 f = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen 𝒜 f).toSpecΓ (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Proj.awayToSection 𝒜 f)) - AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))) = CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm') - AlgebraicGeometry.Proj.awayι_toSpecZero 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.toSpecZero 𝒜) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers f))) - AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst_assoc 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) h - AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd_assoc 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 g)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))) h - AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) h - AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 g)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) h - AlgebraicGeometry.Proj.awayι_toSpecZero_assoc 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of ↥(𝒜 0)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero 𝒜) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers f)))) h - AlgebraicGeometry.Proj.toSpecZero.eq_1 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : AlgebraicGeometry.Proj.toSpecZero 𝒜 = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj 𝒜).topIso.inv (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Proj 𝒜).isoOfEq ⋯).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 1) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers 1)))))) - AlgebraicGeometry.ValuativeCommSq.mk 📋 Mathlib.AlgebraicGeometry.ValuativeCriterion
{X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (R : Type u) [commRing : CommRing R] [domain : IsDomain R] [valuationRing : ValuationRing R] (K : Type u) [field : Field K] [algebra : Algebra R K] [isFractionRing : IsFractionRing R K] (i₁ : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X) (i₂ : AlgebraicGeometry.Spec (CommRingCat.of R) ⟶ Y) (commSq : CategoryTheory.CommSq i₁ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))) f i₂) : AlgebraicGeometry.ValuativeCommSq f - AlgebraicGeometry.ValuativeCommSq.commSq 📋 Mathlib.AlgebraicGeometry.ValuativeCriterion
{X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (self : AlgebraicGeometry.ValuativeCommSq f) : CategoryTheory.CommSq self.i₁ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap self.R self.K))) f self.i₂ - AlgebraicGeometry.ValuativeCommSq.mk.injEq 📋 Mathlib.AlgebraicGeometry.ValuativeCriterion
{X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (R : Type u) [commRing : CommRing R] [domain : IsDomain R] [valuationRing : ValuationRing R] (K : Type u) [field : Field K] [algebra : Algebra R K] [isFractionRing : IsFractionRing R K] (i₁ : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X) (i₂ : AlgebraicGeometry.Spec (CommRingCat.of R) ⟶ Y) (commSq : CategoryTheory.CommSq i₁ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))) f i₂) (R✝ : Type u) (commRing✝ : CommRing R✝) (domain✝ : IsDomain R✝) (valuationRing✝ : ValuationRing R✝) (K✝ : Type u) (field✝ : Field K✝) (algebra✝ : Algebra R✝ K✝) (isFractionRing✝ : IsFractionRing R✝ K✝) (i₁✝ : AlgebraicGeometry.Spec (CommRingCat.of K✝) ⟶ X) (i₂✝ : AlgebraicGeometry.Spec (CommRingCat.of R✝) ⟶ Y) (commSq✝ : CategoryTheory.CommSq i₁✝ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R✝ K✝))) f i₂✝) : ({ R := R, commRing := commRing, domain := domain, valuationRing := valuationRing, K := K, field := field, algebra := algebra, isFractionRing := isFractionRing, i₁ := i₁, i₂ := i₂, commSq := commSq } = { R := R✝, commRing := commRing✝, domain := domain✝, valuationRing := valuationRing✝, K := K✝, field := field✝, algebra := algebra✝, isFractionRing := isFractionRing✝, i₁ := i₁✝, i₂ := i₂✝, commSq := commSq✝ }) = (R = R✝ ∧ HEq commRing commRing✝ ∧ K = K✝ ∧ HEq field field✝ ∧ HEq algebra algebra✝ ∧ HEq i₁ i₁✝ ∧ HEq i₂ i₂✝) - AlgebraicGeometry.ValuativeCommSq.mk.sizeOf_spec 📋 Mathlib.AlgebraicGeometry.ValuativeCriterion
{X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (R : Type u) [commRing : CommRing R] [domain : IsDomain R] [valuationRing : ValuationRing R] (K : Type u) [field : Field K] [algebra : Algebra R K] [isFractionRing : IsFractionRing R K] (i₁ : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X) (i₂ : AlgebraicGeometry.Spec (CommRingCat.of R) ⟶ Y) (commSq : CategoryTheory.CommSq i₁ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))) f i₂) : sizeOf { R := R, commRing := commRing, domain := domain, valuationRing := valuationRing, K := K, field := field, algebra := algebra, isFractionRing := isFractionRing, i₁ := i₁, i₂ := i₂, commSq := commSq } = 1 + sizeOf R + sizeOf commRing + sizeOf domain + sizeOf valuationRing + sizeOf K + sizeOf field + sizeOf algebra + sizeOf isFractionRing + sizeOf i₁ + sizeOf i₂ + sizeOf commSq - AlgebraicGeometry.spread_out_of_isGermInjective 📋 Mathlib.AlgebraicGeometry.SpreadingOut
{X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] {y : ↑↑Y.toPresheafedSpace} (e : (CategoryTheory.ConcreteCategory.hom sX.base) x = (CategoryTheory.ConcreteCategory.hom sY.base) y) (φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x) (h : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap sY y) φ = CategoryTheory.CategoryStruct.comp (S.presheaf.stalkSpecializes ⋯) (AlgebraicGeometry.Scheme.Hom.stalkMap sX x)) : ∃ U, ∃ (hxU : x ∈ U), ∃ f, CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map φ) (Y.fromSpecStalk y) = CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) f ∧ CategoryTheory.CategoryStruct.comp f sY = CategoryTheory.CategoryStruct.comp U.ι sX
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?bBy main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→and∀) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.
This is Loogle revision 19971e9 serving mathlib revision bce1d65