Loogle!
Result
Found 753 definitions mentioning AlgebraicGeometry.Scheme. Of these, only the first 200 are shown.
- AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Scheme
Type (u_1 + 1) - AlgebraicGeometry.Scheme.empty Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme - AlgebraicGeometry.Scheme.forgetToTop_obj_eq_coe Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme → Prop - AlgebraicGeometry.Scheme.instCategory Mathlib.AlgebraicGeometry.Scheme
CategoryTheory.Category.{u_1, u_1 + 1} AlgebraicGeometry.Scheme - AlgebraicGeometry.Scheme.instEmptyCollection Mathlib.AlgebraicGeometry.Scheme
EmptyCollection AlgebraicGeometry.Scheme - AlgebraicGeometry.Scheme.instInhabited Mathlib.AlgebraicGeometry.Scheme
Inhabited AlgebraicGeometry.Scheme - AlgebraicGeometry.Scheme.specObj Mathlib.AlgebraicGeometry.Scheme
CommRingCat → AlgebraicGeometry.Scheme - AlgebraicGeometry.Scheme.toLocallyRingedSpace Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme → AlgebraicGeometry.LocallyRingedSpace - AlgebraicGeometry.Scheme.Hom Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme → AlgebraicGeometry.Scheme → Type u_1 - AlgebraicGeometry.Scheme.hasCoeToTopCat Mathlib.AlgebraicGeometry.Scheme
CoeOut AlgebraicGeometry.Scheme TopCat - AlgebraicGeometry.Scheme.instCoeSortType Mathlib.AlgebraicGeometry.Scheme
CoeSort AlgebraicGeometry.Scheme (Type u_1) - AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace Mathlib.AlgebraicGeometry.Scheme
CategoryTheory.Functor AlgebraicGeometry.Scheme AlgebraicGeometry.LocallyRingedSpace - AlgebraicGeometry.Scheme.forgetToTop Mathlib.AlgebraicGeometry.Scheme
CategoryTheory.Functor AlgebraicGeometry.Scheme TopCat - AlgebraicGeometry.Scheme.instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.Faithful - AlgebraicGeometry.Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.Full - AlgebraicGeometry.Scheme.Spec Mathlib.AlgebraicGeometry.Scheme
CategoryTheory.Functor CommRingCatᵒᵖ AlgebraicGeometry.Scheme - AlgebraicGeometry.Scheme.Γ Mathlib.AlgebraicGeometry.Scheme
CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ CommRingCat - AlgebraicGeometry.Scheme.sheaf Mathlib.AlgebraicGeometry.Scheme
(X : AlgebraicGeometry.Scheme) → TopCat.Sheaf CommRingCat ↑X.toPresheafedSpace - AlgebraicGeometry.Scheme.specMap Mathlib.AlgebraicGeometry.Scheme
{R S : CommRingCat} → (R ⟶ S) → (AlgebraicGeometry.Scheme.specObj S ⟶ AlgebraicGeometry.Scheme.specObj R) - AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_obj Mathlib.AlgebraicGeometry.Scheme
∀ (self : AlgebraicGeometry.Scheme), AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.obj self = self.toLocallyRingedSpace - AlgebraicGeometry.Scheme.is_locallyRingedSpace_iso Mathlib.AlgebraicGeometry.Scheme
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f], CategoryTheory.IsIso f - AlgebraicGeometry.Scheme.specMap_id Mathlib.AlgebraicGeometry.Scheme
∀ (R : CommRingCat), AlgebraicGeometry.Scheme.specMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Scheme.specObj R) - AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_preimage Mathlib.AlgebraicGeometry.Scheme
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.preimage f = f - AlgebraicGeometry.Scheme.Γ_def Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Γ = (CategoryTheory.inducedFunctor AlgebraicGeometry.Scheme.toLocallyRingedSpace).op.comp AlgebraicGeometry.LocallyRingedSpace.Γ - AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_map Mathlib.AlgebraicGeometry.Scheme
∀ {X Y : CategoryTheory.InducedCategory AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace} (f : X ⟶ Y), AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.map f = f - AlgebraicGeometry.Scheme.forgetToTop_obj Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme), AlgebraicGeometry.Scheme.forgetToTop.obj X = (AlgebraicGeometry.SheafedSpace.forget CommRingCat).obj X.toSheafedSpace - AlgebraicGeometry.Scheme.specMap_comp Mathlib.AlgebraicGeometry.Scheme
∀ {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T), AlgebraicGeometry.Scheme.specMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.specMap g) (AlgebraicGeometry.Scheme.specMap f) - AlgebraicGeometry.Scheme.id_val_base Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme), (CategoryTheory.CategoryStruct.id X).val.base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace - AlgebraicGeometry.Scheme.comp_val Mathlib.AlgebraicGeometry.Scheme
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val - AlgebraicGeometry.Scheme.comp_val_assoc Mathlib.AlgebraicGeometry.Scheme
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : AlgebraicGeometry.SheafedSpace CommRingCat} (h : Z.toSheafedSpace ⟶ Z_1), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).val h = CategoryTheory.CategoryStruct.comp f.val (CategoryTheory.CategoryStruct.comp g.val h) - AlgebraicGeometry.Scheme.comp_coeBase Mathlib.AlgebraicGeometry.Scheme
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).val.base = CategoryTheory.CategoryStruct.comp f.val.base g.val.base - AlgebraicGeometry.Scheme.comp_val_base Mathlib.AlgebraicGeometry.Scheme
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).val.base = CategoryTheory.CategoryStruct.comp f.val.base g.val.base - AlgebraicGeometry.Scheme.comp_coeBase_assoc Mathlib.AlgebraicGeometry.Scheme
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : TopCat} (h : ↑Z.toPresheafedSpace ⟶ Z_1), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).val.base h = CategoryTheory.CategoryStruct.comp f.val.base (CategoryTheory.CategoryStruct.comp g.val.base h) - AlgebraicGeometry.Scheme.comp_val_base_assoc Mathlib.AlgebraicGeometry.Scheme
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : TopCat} (h : ↑Z.toPresheafedSpace ⟶ Z_1), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).val.base h = CategoryTheory.CategoryStruct.comp f.val.base (CategoryTheory.CategoryStruct.comp g.val.base h) - AlgebraicGeometry.Scheme.forgetToTop_map Mathlib.AlgebraicGeometry.Scheme
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), AlgebraicGeometry.Scheme.forgetToTop.map f = (AlgebraicGeometry.SheafedSpace.forget CommRingCat).map f.val - AlgebraicGeometry.Scheme.Hom.continuous Mathlib.AlgebraicGeometry.Scheme
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), Continuous ⇑f.val.base - AlgebraicGeometry.Scheme.mk Mathlib.AlgebraicGeometry.Scheme
(toLocallyRingedSpace : AlgebraicGeometry.LocallyRingedSpace) → (∀ (x : ↑toLocallyRingedSpace.toTopCat), ∃ U R, Nonempty (toLocallyRingedSpace.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj { unop := R })) → AlgebraicGeometry.Scheme - AlgebraicGeometry.Scheme.mk.sizeOf_spec Mathlib.AlgebraicGeometry.Scheme
∀ (toLocallyRingedSpace : AlgebraicGeometry.LocallyRingedSpace) (local_affine : ∀ (x : ↑toLocallyRingedSpace.toTopCat), ∃ U R, Nonempty (toLocallyRingedSpace.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj { unop := R })), sizeOf { toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine } = 1 + sizeOf toLocallyRingedSpace - AlgebraicGeometry.Scheme.local_affine Mathlib.AlgebraicGeometry.Scheme
∀ (self : AlgebraicGeometry.Scheme) (x : ↑self.toTopCat), ∃ U R, Nonempty (self.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj { unop := R }) - AlgebraicGeometry.Scheme.basicOpen Mathlib.AlgebraicGeometry.Scheme
(X : AlgebraicGeometry.Scheme) → {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} → ↑(X.presheaf.obj { unop := U }) → TopologicalSpace.Opens ↑↑X.toPresheafedSpace - AlgebraicGeometry.Scheme.Γ_map_op Mathlib.AlgebraicGeometry.Scheme
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), AlgebraicGeometry.Scheme.Γ.map f.op = f.val.c.app { unop := ⊤ } - AlgebraicGeometry.Scheme.Γ_obj_op Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme), AlgebraicGeometry.Scheme.Γ.obj { unop := X } = X.presheaf.obj { unop := ⊤ } - AlgebraicGeometry.Scheme.Γ_map Mathlib.AlgebraicGeometry.Scheme
∀ {X Y : AlgebraicGeometry.Schemeᵒᵖ} (f : X ⟶ Y), AlgebraicGeometry.Scheme.Γ.map f = f.unop.val.c.app { unop := ⊤ } - AlgebraicGeometry.Scheme.basicOpen_le Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj { unop := U })), X.basicOpen f ≤ U - AlgebraicGeometry.Scheme.comp_val_base_apply Mathlib.AlgebraicGeometry.Scheme
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑↑X.toPresheafedSpace), (CategoryTheory.CategoryStruct.comp f g).val.base x = g.val.base (f.val.base x) - AlgebraicGeometry.Scheme.Γ_obj Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Schemeᵒᵖ), AlgebraicGeometry.Scheme.Γ.obj X = X.unop.presheaf.obj { unop := ⊤ } - AlgebraicGeometry.Scheme.mk.injEq Mathlib.AlgebraicGeometry.Scheme
∀ (toLocallyRingedSpace : AlgebraicGeometry.LocallyRingedSpace) (local_affine : ∀ (x : ↑toLocallyRingedSpace.toTopCat), ∃ U R, Nonempty (toLocallyRingedSpace.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj { unop := R })) (toLocallyRingedSpace_1 : AlgebraicGeometry.LocallyRingedSpace) (local_affine_1 : ∀ (x : ↑toLocallyRingedSpace_1.toTopCat), ∃ U R, Nonempty (toLocallyRingedSpace_1.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj { unop := R })), ({ toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine } = { toLocallyRingedSpace := toLocallyRingedSpace_1, local_affine := local_affine_1 }) = (toLocallyRingedSpace = toLocallyRingedSpace_1) - AlgebraicGeometry.Scheme.basicOpen_restrict Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme) {V U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (i : V ⟶ U) (f : ↑(X.presheaf.obj { unop := U })), X.basicOpen (TopCat.Presheaf.restrict f i) ≤ X.basicOpen f - AlgebraicGeometry.Scheme.instIsIsoCommRingCatAppOppositeOpensαTopologicalSpaceCarrierCVal Mathlib.AlgebraicGeometry.Scheme
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] (U : (TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)ᵒᵖ), CategoryTheory.IsIso (f.val.c.app U) - AlgebraicGeometry.basicOpen_eq_of_affine Mathlib.AlgebraicGeometry.Scheme
∀ {R : CommRingCat} (f : ↑R), (AlgebraicGeometry.Scheme.Spec.obj { unop := R }).basicOpen ((AlgebraicGeometry.SpecΓIdentity.app R).inv f) = PrimeSpectrum.basicOpen f - AlgebraicGeometry.Scheme.Hom.appLe Mathlib.AlgebraicGeometry.Scheme
{X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} → {U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} → V ≤ f⁻¹ᵁ U → (Y.presheaf.obj { unop := U } ⟶ X.presheaf.obj { unop := V }) - AlgebraicGeometry.Scheme.id_app Mathlib.AlgebraicGeometry.Scheme
∀ {X : AlgebraicGeometry.Scheme} (U : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ), (CategoryTheory.CategoryStruct.id X).val.c.app U = X.presheaf.map (CategoryTheory.eqToHom ⋯) - AlgebraicGeometry.Scheme.basicOpen_zero Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace), X.basicOpen 0 = ⊥ - AlgebraicGeometry.Scheme.inv_val_c_app_top Mathlib.AlgebraicGeometry.Scheme
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f], (CategoryTheory.inv f).val.c.app { unop := ⊤ } = CategoryTheory.inv (f.val.c.app { unop := ⊤ }) - AlgebraicGeometry.basicOpen_eq_of_affine' Mathlib.AlgebraicGeometry.Scheme
∀ {R : CommRingCat} (f : ↑((AlgebraicGeometry.Spec.toSheafedSpace.obj { unop := R }).presheaf.obj { unop := ⊤ })), (AlgebraicGeometry.Scheme.Spec.obj { unop := R }).basicOpen f = PrimeSpectrum.basicOpen ((AlgebraicGeometry.SpecΓIdentity.app R).hom f) - AlgebraicGeometry.Scheme.basicOpen_of_isUnit Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {f : ↑(X.presheaf.obj { unop := U })}, IsUnit f → X.basicOpen f = U - AlgebraicGeometry.Scheme.algebra_section_section_basicOpen Mathlib.AlgebraicGeometry.Scheme
{X : AlgebraicGeometry.Scheme} → {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} → (f : ↑(X.presheaf.obj { unop := U })) → Algebra ↑(X.presheaf.obj { unop := U }) ↑(X.presheaf.obj { unop := X.basicOpen f }) - AlgebraicGeometry.Scheme.presheaf_map_eqToHom_op Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme) (U V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (i : U = V), X.presheaf.map (CategoryTheory.eqToHom i).op = CategoryTheory.eqToHom ⋯ - AlgebraicGeometry.Scheme.mem_basicOpen Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj { unop := U })) (x : ↥U), ↑x ∈ X.basicOpen f ↔ IsUnit ((X.presheaf.germ x) f) - AlgebraicGeometry.Scheme.basicOpen_res Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme) {V U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj { unop := U })) (i : { unop := U } ⟶ { unop := V }), X.basicOpen ((X.presheaf.map i) f) = V ⊓ X.basicOpen f - AlgebraicGeometry.Scheme.basicOpen_res_eq Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme) {V U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj { unop := U })) (i : { unop := U } ⟶ { unop := V }) [inst : CategoryTheory.IsIso i], X.basicOpen ((X.presheaf.map i) f) = X.basicOpen f - AlgebraicGeometry.Scheme.mem_basicOpen_top' Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj { unop := U })) (x : ↑↑X.toPresheafedSpace), x ∈ X.basicOpen f ↔ ∃ (m : x ∈ U), IsUnit ((X.presheaf.germ ⟨x, m⟩) f) - AlgebraicGeometry.Scheme.basicOpen_mul Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f g : ↑(X.presheaf.obj { unop := U })), X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g - AlgebraicGeometry.Scheme.comp_val_c_app Mathlib.AlgebraicGeometry.Scheme
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑↑Z.toPresheafedSpace)ᵒᵖ), (CategoryTheory.CategoryStruct.comp f g).val.c.app U = CategoryTheory.CategoryStruct.comp (g.val.c.app U) (f.val.c.app ((TopologicalSpace.Opens.map g.val.base).op.obj U)) - AlgebraicGeometry.Scheme.preimage_basicOpen Mathlib.AlgebraicGeometry.Scheme
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} (r : ↑(Y.presheaf.obj { unop := U })), f⁻¹ᵁ Y.basicOpen r = X.basicOpen ((f.val.c.app { unop := U }) r) - AlgebraicGeometry.Scheme.comp_val_c_app_assoc Mathlib.AlgebraicGeometry.Scheme
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑↑Z.toPresheafedSpace)ᵒᵖ) {Z_1 : CommRingCat} (h : ((CategoryTheory.CategoryStruct.comp f g).val.base _* X.presheaf).obj U ⟶ Z_1), CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f g).val.c.app U) h = CategoryTheory.CategoryStruct.comp (g.val.c.app U) (CategoryTheory.CategoryStruct.comp (f.val.c.app ((TopologicalSpace.Opens.map g.val.base).op.obj U)) h) - AlgebraicGeometry.Scheme.mem_basicOpen_top Mathlib.AlgebraicGeometry.Scheme
∀ (X : AlgebraicGeometry.Scheme) (f : ↑(X.presheaf.obj { unop := ⊤ })) (x : ↑↑X.toPresheafedSpace), x ∈ X.basicOpen f ↔ IsUnit ((X.presheaf.germ ⟨x, trivial⟩) f) - AlgebraicGeometry.Scheme.congr_app Mathlib.AlgebraicGeometry.Scheme
∀ {X Y : AlgebraicGeometry.Scheme} {f g : X ⟶ Y} (e : f = g) (U : (TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)ᵒᵖ), f.val.c.app U = CategoryTheory.CategoryStruct.comp (g.val.c.app U) (X.presheaf.map (CategoryTheory.eqToHom ⋯)) - AlgebraicGeometry.Scheme.app_eq Mathlib.AlgebraicGeometry.Scheme
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U V : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} (e : U = V), f.val.c.app { unop := U } = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) (CategoryTheory.CategoryStruct.comp (f.val.c.app { unop := V }) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)) - AlgebraicGeometry.Scheme.inv_val_c_app Mathlib.AlgebraicGeometry.Scheme
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace), (CategoryTheory.inv f).val.c.app { unop := U } = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯).op) (CategoryTheory.inv (f.val.c.app { unop := CategoryTheory.inv f⁻¹ᵁ U })) - AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom Mathlib.AlgebraicGeometry.Scheme
∀ {X : AlgebraicGeometry.Scheme} {U V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (h : U = V) (W : (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Scheme.Spec.obj { unop := X.presheaf.obj { unop := V } }).toPresheafedSpace)ᵒᵖ), (AlgebraicGeometry.Scheme.Spec.map (X.presheaf.map (CategoryTheory.eqToHom h).op).op).val.c.app W = CategoryTheory.eqToHom ⋯ - AlgebraicGeometry.Scheme.AffineOpenCover Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme → Type (max (u + 1) (v + 1)) - AlgebraicGeometry.Scheme.OpenCover Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme → Type (max (u + 1) (v + 1)) - AlgebraicGeometry.Scheme.affineBasisCover Mathlib.AlgebraicGeometry.OpenImmersion
(X : AlgebraicGeometry.Scheme) → X.OpenCover - AlgebraicGeometry.Scheme.affineCover Mathlib.AlgebraicGeometry.OpenImmersion
(X : AlgebraicGeometry.Scheme) → X.OpenCover - AlgebraicGeometry.Scheme.affineOpenCover Mathlib.AlgebraicGeometry.OpenImmersion
(X : AlgebraicGeometry.Scheme) → X.AffineOpenCover - AlgebraicGeometry.Scheme.instInhabitedOpenCover Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → Inhabited X.OpenCover - AlgebraicGeometry.Scheme.AffineOpenCover.J Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → X.AffineOpenCover → Type v - AlgebraicGeometry.Scheme.OpenCover.J Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → X.OpenCover → Type v - AlgebraicGeometry.Scheme.OpenCover.category Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → CategoryTheory.Category.{max u v, max (v + 1) (u + 1)} X.OpenCover - AlgebraicGeometry.Scheme.AffineOpenCover.openCover Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → X.AffineOpenCover → X.OpenCover - AlgebraicGeometry.Scheme.OpenCover.affineRefinement Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → X.OpenCover → X.AffineOpenCover - AlgebraicGeometry.Scheme.affineBasisCoverRing Mathlib.AlgebraicGeometry.OpenImmersion
(X : AlgebraicGeometry.Scheme) → X.affineBasisCover.J → CommRingCat - AlgebraicGeometry.Scheme.OpenCover.Hom Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → X.OpenCover → X.OpenCover → Type (max u v) - AlgebraicGeometry.Scheme.AffineOpenCover.obj Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → (self : X.AffineOpenCover) → self.J → CommRingCat - AlgebraicGeometry.Scheme.OpenCover.inter Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → X.OpenCover → X.OpenCover → X.OpenCover - AlgebraicGeometry.Scheme.OpenCover.obj Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → (self : X.OpenCover) → self.J → AlgebraicGeometry.Scheme - AlgebraicGeometry.Scheme.OpenCover.Hom.id Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → (𝓤 : X.OpenCover) → 𝓤.Hom 𝓤 - AlgebraicGeometry.Scheme.openCover_affineOpenCover Mathlib.AlgebraicGeometry.OpenImmersion
∀ (X : AlgebraicGeometry.Scheme), X.affineOpenCover.openCover = X.affineCover - AlgebraicGeometry.IsOpenImmersion Mathlib.AlgebraicGeometry.OpenImmersion
{X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop - AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_eq_of_locallyRingedSpace_eq Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme}, X.toLocallyRingedSpace = Y.toLocallyRingedSpace → X = Y - AlgebraicGeometry.Scheme.AffineOpenCover.openCover_J Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover), 𝓤.openCover.J = 𝓤.J - AlgebraicGeometry.Scheme.OpenCover.bind Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → (𝒰 : X.OpenCover) → ((x : 𝒰.J) → (𝒰.obj x).OpenCover) → X.OpenCover - AlgebraicGeometry.Scheme.OpenCover.pullbackCover Mathlib.AlgebraicGeometry.OpenImmersion
{X W : AlgebraicGeometry.Scheme} → X.OpenCover → (W ⟶ X) → W.OpenCover - AlgebraicGeometry.Scheme.OpenCover.pullbackCover' Mathlib.AlgebraicGeometry.OpenImmersion
{X W : AlgebraicGeometry.Scheme} → X.OpenCover → (W ⟶ X) → W.OpenCover - AlgebraicGeometry.Scheme.OpenCover.Hom.idx Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → {𝓤 𝓥 : X.OpenCover} → 𝓤.Hom 𝓥 → 𝓤.J → 𝓥.J - AlgebraicGeometry.Scheme.OpenCover.IsOpen Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (self : X.OpenCover) (x : self.J), AlgebraicGeometry.IsOpenImmersion (self.map x) - AlgebraicGeometry.Scheme.AffineOpenCover.f Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → (self : X.AffineOpenCover) → ↑↑X.toPresheafedSpace → self.J - AlgebraicGeometry.Scheme.OpenCover.f Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → (self : X.OpenCover) → ↑↑X.toPresheafedSpace → self.J - AlgebraicGeometry.Scheme.OpenCover.map Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → (self : X.OpenCover) → (j : self.J) → self.obj j ⟶ X - AlgebraicGeometry.Scheme.openCoverOfIsIso Mathlib.AlgebraicGeometry.OpenImmersion
{X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → [inst : CategoryTheory.IsIso f] → Y.OpenCover - AlgebraicGeometry.Scheme.OpenCover.add Mathlib.AlgebraicGeometry.OpenImmersion
{X Y : AlgebraicGeometry.Scheme} → X.OpenCover → (f : Y ⟶ X) → [inst : AlgebraicGeometry.IsOpenImmersion f] → X.OpenCover - AlgebraicGeometry.Scheme.OpenCover.Hom.comp Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → {𝓤 𝓥 𝓦 : X.OpenCover} → 𝓤.Hom 𝓥 → 𝓥.Hom 𝓦 → 𝓤.Hom 𝓦 - AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → (𝓤 : X.OpenCover) → 𝓤.affineRefinement.openCover ⟶ 𝓤 - AlgebraicGeometry.IsOpenImmersion.mono Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f], CategoryTheory.Mono f - AlgebraicGeometry.IsOpenImmersion.of_isIso Mathlib.AlgebraicGeometry.OpenImmersion
∀ {Y Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z) [inst : CategoryTheory.IsIso g], AlgebraicGeometry.IsOpenImmersion g - AlgebraicGeometry.Scheme.OpenCover.pushforwardIso Mathlib.AlgebraicGeometry.OpenImmersion
{X Y : AlgebraicGeometry.Scheme} → X.OpenCover → (f : X ⟶ Y) → [inst : CategoryTheory.IsIso f] → Y.OpenCover - AlgebraicGeometry.Scheme.OpenCover.finiteSubcover Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → X.OpenCover → [H : CompactSpace ↑↑X.toPresheafedSpace] → X.OpenCover - AlgebraicGeometry.Scheme.OpenCover.id_idx_apply Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝓤 : X.OpenCover) (j : 𝓤.J), (CategoryTheory.CategoryStruct.id 𝓤).idx j = j - AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_J Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X), (𝒰.pullbackCover' f).J = 𝒰.J - AlgebraicGeometry.Scheme.OpenCover.pullbackCover_J Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X), (𝒰.pullbackCover f).J = 𝒰.J - AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover) (a : ↑↑X.toPresheafedSpace), 𝓤.openCover.f a = 𝓤.f a - AlgebraicGeometry.Scheme.openCoverOfIsIso_J Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f], (AlgebraicGeometry.Scheme.openCoverOfIsIso f).J = PUnit.{v + 1} - AlgebraicGeometry.Scheme.instFintypeJFiniteSubcover Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → (𝒰 : X.OpenCover) → [H : CompactSpace ↑↑X.toPresheafedSpace] → Fintype 𝒰.finiteSubcover.J - AlgebraicGeometry.Scheme.openCoverOfIsIso_obj Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] (x : PUnit.{v + 1}), (AlgebraicGeometry.Scheme.openCoverOfIsIso f).obj x = X - AlgebraicGeometry.Scheme.OpenCover.add_J Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : Y ⟶ X) [inst : AlgebraicGeometry.IsOpenImmersion f], (𝒰.add f).J = Option 𝒰.J - AlgebraicGeometry.Scheme.affineBasisCoverOfAffine Mathlib.AlgebraicGeometry.OpenImmersion
(R : CommRingCat) → (AlgebraicGeometry.Scheme.Spec.obj { unop := R }).OpenCover - AlgebraicGeometry.Scheme.OpenCover.pushforwardIso_J Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Y) [inst : CategoryTheory.IsIso f], (𝒰.pushforwardIso f).J = 𝒰.J - AlgebraicGeometry.Scheme.OpenCover.Hom.app Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → {𝓤 𝓥 : X.OpenCover} → (self : 𝓤.Hom 𝓥) → (j : 𝓤.J) → 𝓤.obj j ⟶ 𝓥.obj (self.idx j) - AlgebraicGeometry.Scheme.OpenCover.Hom.isOpen Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} {𝓤 𝓥 : X.OpenCover} (self : 𝓤.Hom 𝓥) (j : 𝓤.J), AlgebraicGeometry.IsOpenImmersion (self.app j) - AlgebraicGeometry.IsOpenImmersion.hasPullback_of_left Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f], CategoryTheory.Limits.HasPullback f g - AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f], CategoryTheory.Limits.HasPullback g f - AlgebraicGeometry.Scheme.openCoverOfIsIso_map Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] (x : PUnit.{v + 1}), (AlgebraicGeometry.Scheme.openCoverOfIsIso f).map x = f - AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_toScheme Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f], AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme Y f.val = X - AlgebraicGeometry.Scheme.Hom.opensRange Mathlib.AlgebraicGeometry.OpenImmersion
{X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → [H : AlgebraicGeometry.IsOpenImmersion f] → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace - AlgebraicGeometry.Scheme.OpenCover.bind_J Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : (x : 𝒰.J) → (𝒰.obj x).OpenCover), (𝒰.bind f).J = ((i : 𝒰.J) × (f i).J) - AlgebraicGeometry.Scheme.OpenCover.pushforwardIso_obj Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] (x : 𝒰.J), (𝒰.pushforwardIso f).obj x = 𝒰.obj x - AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.PresheafedSpace CommRingCat} → (Y : AlgebraicGeometry.Scheme) → (f : X ⟶ Y.toPresheafedSpace) → [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] → AlgebraicGeometry.Scheme - AlgebraicGeometry.IsOpenImmersion.comp Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsOpenImmersion f] [inst : AlgebraicGeometry.IsOpenImmersion g], AlgebraicGeometry.IsOpenImmersion (CategoryTheory.CategoryStruct.comp f g) - AlgebraicGeometry.IsOpenImmersion.forgetCreatesPullbackOfLeft Mathlib.AlgebraicGeometry.OpenImmersion
{X Y Z : AlgebraicGeometry.Scheme} → (f : X ⟶ Z) → (g : Y ⟶ Z) → [H : AlgebraicGeometry.IsOpenImmersion f] → CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan f g) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace - AlgebraicGeometry.IsOpenImmersion.forgetCreatesPullbackOfRight Mathlib.AlgebraicGeometry.OpenImmersion
{X Y Z : AlgebraicGeometry.Scheme} → (f : X ⟶ Z) → (g : Y ⟶ Z) → [H : AlgebraicGeometry.IsOpenImmersion f] → CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan g f) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace - AlgebraicGeometry.IsOpenImmersion.forgetPreservesOfLeft Mathlib.AlgebraicGeometry.OpenImmersion
{X Y Z : AlgebraicGeometry.Scheme} → (f : X ⟶ Z) → (g : Y ⟶ Z) → [H : AlgebraicGeometry.IsOpenImmersion f] → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace - AlgebraicGeometry.IsOpenImmersion.forgetPreservesOfRight Mathlib.AlgebraicGeometry.OpenImmersion
{X Y Z : AlgebraicGeometry.Scheme} → (f : X ⟶ Z) → (g : Y ⟶ Z) → [H : AlgebraicGeometry.IsOpenImmersion f] → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace - AlgebraicGeometry.IsOpenImmersion.forgetToTopPreservesOfLeft Mathlib.AlgebraicGeometry.OpenImmersion
{X Y Z : AlgebraicGeometry.Scheme} → (f : X ⟶ Z) → (g : Y ⟶ Z) → [H : AlgebraicGeometry.IsOpenImmersion f] → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) AlgebraicGeometry.Scheme.forgetToTop - AlgebraicGeometry.IsOpenImmersion.forgetToTopPreservesOfRight Mathlib.AlgebraicGeometry.OpenImmersion
{X Y Z : AlgebraicGeometry.Scheme} → (f : X ⟶ Z) → (g : Y ⟶ Z) → [H : AlgebraicGeometry.IsOpenImmersion f] → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) AlgebraicGeometry.Scheme.forgetToTop - AlgebraicGeometry.Scheme.affineBasisCover_obj Mathlib.AlgebraicGeometry.OpenImmersion
∀ (X : AlgebraicGeometry.Scheme) (i : X.affineBasisCover.J), X.affineBasisCover.obj i = AlgebraicGeometry.Scheme.Spec.obj { unop := X.affineBasisCoverRing i } - AlgebraicGeometry.Scheme.AffineOpenCover.IsOpen Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (self : X.AffineOpenCover) (x : self.J), AlgebraicGeometry.IsOpenImmersion (self.map x) - AlgebraicGeometry.Scheme.OpenCover.add_obj Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : Y ⟶ X) [inst : AlgebraicGeometry.IsOpenImmersion f] (i : Option 𝒰.J), (𝒰.add f).obj i = Option.rec Y 𝒰.obj i - AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_obj Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) (x : 𝒰.J), (𝒰.pullbackCover' f).obj x = CategoryTheory.Limits.pullback (𝒰.map x) f - AlgebraicGeometry.Scheme.OpenCover.pullbackCover_obj Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) (x : 𝒰.J), (𝒰.pullbackCover f).obj x = CategoryTheory.Limits.pullback f (𝒰.map x) - AlgebraicGeometry.Scheme.AffineOpenCover.map Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → (self : X.AffineOpenCover) → (j : self.J) → AlgebraicGeometry.Scheme.Spec.obj { unop := self.obj j } ⟶ X - AlgebraicGeometry.Scheme.AffineOpenCover.openCover_obj Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover) (j : 𝓤.J), 𝓤.openCover.obj j = AlgebraicGeometry.Scheme.Spec.obj { unop := 𝓤.obj j } - AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f], CategoryTheory.Limits.HasLimit ((CategoryTheory.Limits.cospan f g).comp AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace) - AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f], CategoryTheory.Limits.HasLimit ((CategoryTheory.Limits.cospan g f).comp AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace) - AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_isOpenImmersion Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y.toPresheafedSpace) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f], AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom Y f) - AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.PresheafedSpace CommRingCat} → (Y : AlgebraicGeometry.Scheme) → (f : X ⟶ Y.toPresheafedSpace) → [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] → AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme Y f ⟶ Y - AlgebraicGeometry.Scheme.OpenCover.add_f Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : Y ⟶ X) [inst : AlgebraicGeometry.IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace), (𝒰.add f).f x = some (𝒰.f x) - AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme_toLocallyRingedSpace Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y.toPresheafedSpace) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f], (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme Y f).toLocallyRingedSpace = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y.toLocallyRingedSpace f - AlgebraicGeometry.Scheme.OpenCover.compactSpace Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [inst : Finite 𝒰.J] [H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace], CompactSpace ↑↑X.toPresheafedSpace - AlgebraicGeometry.Scheme.AffineOpenCover.openCover_map Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover) (j : 𝓤.J), 𝓤.openCover.map j = 𝓤.map j - AlgebraicGeometry.IsOpenImmersion.pullback_fst_of_right Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f], AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback.fst - AlgebraicGeometry.IsOpenImmersion.pullback_snd_of_left Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f], AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback.snd - AlgebraicGeometry.Scheme.OpenCover.id_app Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝓤 : X.OpenCover) (j : 𝓤.J), (CategoryTheory.CategoryStruct.id 𝓤).app j = CategoryTheory.CategoryStruct.id (𝓤.obj j) - AlgebraicGeometry.Scheme.val_base_isIso Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f], CategoryTheory.IsIso f.val.base - AlgebraicGeometry.IsOpenImmersion.to_iso Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [h : AlgebraicGeometry.IsOpenImmersion f] [inst : CategoryTheory.Epi f.val.base], CategoryTheory.IsIso f - AlgebraicGeometry.Scheme.OpenCover.Hom.w Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} {𝓤 𝓥 : X.OpenCover} (self : 𝓤.Hom 𝓥) (j : 𝓤.J), CategoryTheory.CategoryStruct.comp (self.app j) (𝓥.map (self.idx j)) = 𝓤.map j - AlgebraicGeometry.isIso_iff_isOpenImmersion Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), CategoryTheory.IsIso f ↔ AlgebraicGeometry.IsOpenImmersion f ∧ CategoryTheory.Epi f.val.base - AlgebraicGeometry.Scheme.OpenCover.comp_idx_apply Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} {𝓤 𝓥 𝓦 : X.OpenCover} (f : 𝓤 ⟶ 𝓥) (g : 𝓥 ⟶ 𝓦) (j : 𝓤.J), (CategoryTheory.CategoryStruct.comp f g).idx j = g.idx (f.idx j) - AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_map Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) (x : 𝒰.J), (𝒰.pullbackCover' f).map x = CategoryTheory.Limits.pullback.snd - AlgebraicGeometry.Scheme.OpenCover.pullbackCover_map Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) (x : 𝒰.J), (𝒰.pullbackCover f).map x = CategoryTheory.Limits.pullback.fst - AlgebraicGeometry.IsOpenImmersion.isoRestrict Mathlib.AlgebraicGeometry.OpenImmersion
{X Z : AlgebraicGeometry.Scheme} → (f : X ⟶ Z) → [H : AlgebraicGeometry.IsOpenImmersion f] → X ≅ Z.restrict ⋯ - AlgebraicGeometry.IsOpenImmersion.forget_map_isOpenImmersion Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f], AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.map f) - AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_val Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y.toPresheafedSpace) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f], (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom Y f).val = f - AlgebraicGeometry.Scheme.OpenCover.bind_obj Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : (x : 𝒰.J) → (𝒰.obj x).OpenCover) (x : (i : 𝒰.J) × (f i).J), (𝒰.bind f).obj x = (f x.fst).obj x.snd - AlgebraicGeometry.Scheme.OpenCover.add_map Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : Y ⟶ X) [inst : AlgebraicGeometry.IsOpenImmersion f] (i : Option 𝒰.J), (𝒰.add f).map i = Option.rec f 𝒰.map i - AlgebraicGeometry.Scheme.OpenCover.Hom.mk Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → {𝓤 𝓥 : X.OpenCover} → (idx : 𝓤.J → 𝓥.J) → (app : (j : 𝓤.J) → 𝓤.obj j ⟶ 𝓥.obj (idx j)) → autoParam (∀ (j : 𝓤.J), AlgebraicGeometry.IsOpenImmersion (app j)) _auto✝ → autoParam (∀ (j : 𝓤.J), CategoryTheory.CategoryStruct.comp (app j) (𝓥.map (idx j)) = 𝓤.map j) _auto✝¹ → 𝓤.Hom 𝓥 - AlgebraicGeometry.IsOpenImmersion.pullback_to_base Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] [inst : AlgebraicGeometry.IsOpenImmersion g], AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one) - AlgebraicGeometry.Scheme.OpenCover.Hom.w_assoc Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} {𝓤 𝓥 : X.OpenCover} (self : 𝓤.Hom 𝓥) (j : 𝓤.J) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z), CategoryTheory.CategoryStruct.comp (self.app j) (CategoryTheory.CategoryStruct.comp (𝓥.map (self.idx j)) h) = CategoryTheory.CategoryStruct.comp (𝓤.map j) h - AlgebraicGeometry.Scheme.OpenCover.Hom.mk.sizeOf_spec Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} {𝓤 𝓥 : X.OpenCover} (idx : 𝓤.J → 𝓥.J) (app : (j : 𝓤.J) → 𝓤.obj j ⟶ 𝓥.obj (idx j)) (isOpen : autoParam (∀ (j : 𝓤.J), AlgebraicGeometry.IsOpenImmersion (app j)) _auto✝) (w : autoParam (∀ (j : 𝓤.J), CategoryTheory.CategoryStruct.comp (app j) (𝓥.map (idx j)) = 𝓤.map j) _auto✝¹), sizeOf { idx := idx, app := app, isOpen := isOpen, w := w } = 1 - AlgebraicGeometry.Scheme.OpenCover.comp_app Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} {𝓤 𝓥 𝓦 : X.OpenCover} (f : 𝓤 ⟶ 𝓥) (g : 𝓥 ⟶ 𝓦) (j : 𝓤.J), (CategoryTheory.CategoryStruct.comp f g).app j = CategoryTheory.CategoryStruct.comp (f.app j) (g.app (f.idx j)) - AlgebraicGeometry.Scheme.OpenCover.copy Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → (𝒰 : X.OpenCover) → (J : Type u_1) → (obj : J → AlgebraicGeometry.Scheme) → (map : (i : J) → obj i ⟶ X) → (e₁ : J ≃ 𝒰.J) → (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) → (∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.map (e₁ i))) → X.OpenCover - AlgebraicGeometry.Scheme.OpenCover.copy_J Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (e₂_1 : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.map (e₁ i))), (𝒰.copy J obj map e₁ e₂ e₂_1).J = J - AlgebraicGeometry.Scheme.OpenCover.copy_obj Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (e₂_1 : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.map (e₁ i))) (a : J), (𝒰.copy J obj map e₁ e₂ e₂_1).obj a = obj a - AlgebraicGeometry.Scheme.OpenCover.copy_map Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (e₂_1 : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.map (e₁ i))) (i : J), (𝒰.copy J obj map e₁ e₂ e₂_1).map i = map i - AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover), ⨆ i, AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.map i) = ⊤ - AlgebraicGeometry.Scheme.openCoverOfSuprEqTop Mathlib.AlgebraicGeometry.OpenImmersion
{s : Type u_1} → (X : AlgebraicGeometry.Scheme) → (U : s → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) → ⨆ i, U i = ⊤ → X.OpenCover - AlgebraicGeometry.Scheme.openCoverOfSuprEqTop_J Mathlib.AlgebraicGeometry.OpenImmersion
∀ {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hU : ⨆ i, U i = ⊤), (X.openCoverOfSuprEqTop U hU).J = s - AlgebraicGeometry.Scheme.OpenCover.pushforwardIso_map Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] (x : 𝒰.J), (𝒰.pushforwardIso f).map x = CategoryTheory.CategoryStruct.comp (𝒰.map x) f - AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_f Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) (x : ↑↑W.toPresheafedSpace), (𝒰.pullbackCover' f).f x = 𝒰.f (f.val.base x) - AlgebraicGeometry.Scheme.OpenCover.pullbackCover_f Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) (x : ↑↑W.toPresheafedSpace), (𝒰.pullbackCover f).f x = 𝒰.f (f.val.base x) - AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left' Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f], CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan (((CategoryTheory.Limits.cospan f g).comp AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inl) (((CategoryTheory.Limits.cospan f g).comp AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inr)) - AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right' Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f], CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan (((CategoryTheory.Limits.cospan g f).comp AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inl) (((CategoryTheory.Limits.cospan g f).comp AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inr)) - AlgebraicGeometry.Scheme.Hom.opensFunctor Mathlib.AlgebraicGeometry.OpenImmersion
{X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → [H : AlgebraicGeometry.IsOpenImmersion f] → CategoryTheory.Functor (TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) - AlgebraicGeometry.Scheme.OpenCover.bind_map Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : (x : 𝒰.J) → (𝒰.obj x).OpenCover) (x : (i : 𝒰.J) × (f i).J), (𝒰.bind f).map x = CategoryTheory.CategoryStruct.comp ((f x.fst).map x.snd) (𝒰.map x.fst) - AlgebraicGeometry.Scheme.restrict Mathlib.AlgebraicGeometry.OpenImmersion
{U : TopCat} → (X : AlgebraicGeometry.Scheme) → {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} → OpenEmbedding ⇑f → AlgebraicGeometry.Scheme - AlgebraicGeometry.Scheme.OpenCover.Hom.mk.injEq Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} {𝓤 𝓥 : X.OpenCover} (idx : 𝓤.J → 𝓥.J) (app : (j : 𝓤.J) → 𝓤.obj j ⟶ 𝓥.obj (idx j)) (isOpen : autoParam (∀ (j : 𝓤.J), AlgebraicGeometry.IsOpenImmersion (app j)) _auto✝) (w : autoParam (∀ (j : 𝓤.J), CategoryTheory.CategoryStruct.comp (app j) (𝓥.map (idx j)) = 𝓤.map j) _auto✝¹) (idx_1 : 𝓤.J → 𝓥.J) (app_1 : (j : 𝓤.J) → 𝓤.obj j ⟶ 𝓥.obj (idx_1 j)) (isOpen_1 : autoParam (∀ (j : 𝓤.J), AlgebraicGeometry.IsOpenImmersion (app_1 j)) _auto✝) (w_1 : autoParam (∀ (j : 𝓤.J), CategoryTheory.CategoryStruct.comp (app_1 j) (𝓥.map (idx_1 j)) = 𝓤.map j) _auto✝¹), ({ idx := idx, app := app, isOpen := isOpen, w := w } = { idx := idx_1, app := app_1, isOpen := isOpen_1, w := w_1 }) = (idx = idx_1 ∧ HEq app app_1) - AlgebraicGeometry.IsOpenImmersion.ofRestrict Mathlib.AlgebraicGeometry.OpenImmersion
∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : OpenEmbedding ⇑f), AlgebraicGeometry.IsOpenImmersion (X.ofRestrict h) - AlgebraicGeometry.Scheme.ofRestrict Mathlib.AlgebraicGeometry.OpenImmersion
{U : TopCat} → (X : AlgebraicGeometry.Scheme) → {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} → (h : OpenEmbedding ⇑f) → X.restrict h ⟶ X - AlgebraicGeometry.Scheme.restrict_carrier Mathlib.AlgebraicGeometry.OpenImmersion
∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : OpenEmbedding ⇑f), ↑(X.restrict h).toPresheafedSpace = U - AlgebraicGeometry.Scheme.restrict_toPresheafedSpace Mathlib.AlgebraicGeometry.OpenImmersion
∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : OpenEmbedding ⇑f), (X.restrict h).toPresheafedSpace = X.restrict h - AlgebraicGeometry.isIso_iff_stalk_iso Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.stalkMap f.val x) - AlgebraicGeometry.IsOpenImmersion.isOpen_range Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f], IsOpen (Set.range ⇑f.val.base) - AlgebraicGeometry.IsOpenImmersion.open_range Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f], IsOpen (Set.range ⇑f.val.base) - AlgebraicGeometry.Scheme.affineBasisCover_is_basis Mathlib.AlgebraicGeometry.OpenImmersion
∀ (X : AlgebraicGeometry.Scheme), TopologicalSpace.IsTopologicalBasis {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.map a).val.base} - AlgebraicGeometry.Scheme.Hom.opensRange_coe Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f], ↑(AlgebraicGeometry.Scheme.Hom.opensRange f) = Set.range ⇑f.val.base - AlgebraicGeometry.Scheme.ofRestrict_val_base Mathlib.AlgebraicGeometry.OpenImmersion
∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : OpenEmbedding ⇑f), (X.ofRestrict h).val.base = f - AlgebraicGeometry.Scheme.OpenCover.iUnion_range Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover), ⋃ i, Set.range ⇑(𝒰.map i).val.base = Set.univ - AlgebraicGeometry.Scheme.basic_open_isOpenImmersion Mathlib.AlgebraicGeometry.OpenImmersion
∀ {R : CommRingCat} (f : ↑R), AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))).op) - AlgebraicGeometry.Scheme.OpenCover.Covers Mathlib.AlgebraicGeometry.OpenImmersion
∀ {X : AlgebraicGeometry.Scheme} (self : X.OpenCover) (x : ↑↑X.toPresheafedSpace), x ∈ Set.range ⇑(self.map (self.f x)).val.base - AlgebraicGeometry.Scheme.OpenCover.mk Mathlib.AlgebraicGeometry.OpenImmersion
{X : AlgebraicGeometry.Scheme} → (J : Type v) → (obj : J → AlgebraicGeometry.Scheme) → (map : (j : J) → obj j ⟶ X) → (f : ↑↑X.toPresheafedSpace → J) → (∀ (x : ↑↑X.toPresheafedSpace), x ∈ Set.range ⇑(map (f x)).val.base) → autoParam (∀ (x : J), AlgebraicGeometry.IsOpenImmersion (map x)) _auto✝ → X.OpenCover
Did you maybe mean
About
Loogle searches of Lean and Mathlib definitions and theorems.
You may also want to try the CLI version, the 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 ?a
If 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 ?b
By 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_tsum
even though the hypothesisf i < g i
is 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, _ * _, _ ^ _, |- _ < _ → _
woould 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 currently provided by Joachim Breitner <mail@joachim-breitner.de>.
This is Loogle revision fa2ddf5
serving mathlib revision c44d42e