-
-
Save kbuzzard/54cffdba7c4c880fe6bc4c1d2d364765 to your computer and use it in GitHub Desktop.
unfolding a 40 second rewrite reveals that it's a bunch of things which take a couple of seconds, and 35+ missing seconds.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| [] [40.743137s] rewrite [morphismRestrict_c_app, Category.assoc, Category.assoc, Category.assoc] ▼ | |
| [Meta.check] [0.102614s] ✅ fun _a ↦ | |
| ((CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict Y | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).val.c | |
| (Opposite.op ⊤) ≫ | |
| CategoryTheory.NatTrans.app (f ∣_ AlgebraicGeometry.Scheme.basicOpen Y r).val.c | |
| (Opposite.op ⊤)) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict | |
| (AlgebraicGeometry.Scheme.restrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))) | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y | |
| r))))).val.base).obj | |
| U)))).val.c | |
| (Opposite.op ⊤) = | |
| (CategoryTheory.NatTrans.app f.val.c (Opposite.op ⊤) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U))).val.c | |
| (Opposite.op ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.homOfLE | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen | |
| Y r))))).val.base).obj | |
| U)))).op.obj | |
| (Opposite.op ⊤)).unop ≤ | |
| (IsOpenMap.functor (_ : IsOpenMap ↑(TopologicalSpace.Opens.inclusion U))).obj | |
| (Opposite.op ⊤).unop)).op) = | |
| ((CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict Y | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).val.c | |
| (Opposite.op ⊤) ≫ | |
| _a) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict | |
| (AlgebraicGeometry.Scheme.restrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))) | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y | |
| r))))).val.base).obj | |
| U)))).val.c | |
| (Opposite.op ⊤) = | |
| (CategoryTheory.NatTrans.app f.val.c (Opposite.op ⊤) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U))).val.c | |
| (Opposite.op ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.homOfLE | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen | |
| Y r))))).val.base).obj | |
| U)))).op.obj | |
| (Opposite.op ⊤)).unop ≤ | |
| (IsOpenMap.functor (_ : IsOpenMap ↑(TopologicalSpace.Opens.inclusion U))).obj | |
| (Opposite.op ⊤).unop)).op) ▶ | |
| [Meta.isDefEq] [0.052403s] ✅ (CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict Y | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).val.c | |
| (Opposite.op ⊤) ≫ | |
| CategoryTheory.NatTrans.app f.val.c | |
| (Opposite.op | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).obj | |
| ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.eqToHom | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((TopologicalSpace.Opens.map | |
| (f ∣_ AlgebraicGeometry.Scheme.basicOpen Y r).val.base).obj | |
| ⊤) = | |
| (TopologicalSpace.Opens.map f.val.base).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).obj | |
| ⊤))).op) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict | |
| (AlgebraicGeometry.Scheme.restrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))) | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y | |
| r))))).val.base).obj | |
| U)))).val.c | |
| (Opposite.op ⊤) =?= (?f ≫ ?g) ≫ ?h ▶ | |
| [Meta.check] [0.083009s] ✅ fun _a ↦ | |
| ((CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict Y | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).val.c | |
| (Opposite.op ⊤) ≫ | |
| CategoryTheory.NatTrans.app f.val.c | |
| (Opposite.op | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).obj | |
| ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.eqToHom | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((TopologicalSpace.Opens.map | |
| (f ∣_ AlgebraicGeometry.Scheme.basicOpen Y r).val.base).obj | |
| ⊤) = | |
| (TopologicalSpace.Opens.map f.val.base).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).obj | |
| ⊤))).op) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict | |
| (AlgebraicGeometry.Scheme.restrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))) | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y | |
| r))))).val.base).obj | |
| U)))).val.c | |
| (Opposite.op ⊤) = | |
| (CategoryTheory.NatTrans.app f.val.c (Opposite.op ⊤) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U))).val.c | |
| (Opposite.op ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.homOfLE | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen | |
| Y r))))).val.base).obj | |
| U)))).op.obj | |
| (Opposite.op ⊤)).unop ≤ | |
| (IsOpenMap.functor (_ : IsOpenMap ↑(TopologicalSpace.Opens.inclusion U))).obj | |
| (Opposite.op ⊤).unop)).op) = | |
| (_a = | |
| (CategoryTheory.NatTrans.app f.val.c (Opposite.op ⊤) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U))).val.c | |
| (Opposite.op ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.homOfLE | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen | |
| Y r))))).val.base).obj | |
| U)))).op.obj | |
| (Opposite.op ⊤)).unop ≤ | |
| (IsOpenMap.functor (_ : IsOpenMap ↑(TopologicalSpace.Opens.inclusion U))).obj | |
| (Opposite.op ⊤).unop)).op) ▶ | |
| [Meta.isDefEq] [0.044169s] ✅ (CategoryTheory.NatTrans.app f.val.c | |
| (Opposite.op | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).obj | |
| ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.eqToHom | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((TopologicalSpace.Opens.map | |
| (f ∣_ AlgebraicGeometry.Scheme.basicOpen Y r).val.base).obj | |
| ⊤) = | |
| (TopologicalSpace.Opens.map f.val.base).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).obj | |
| ⊤))).op) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict | |
| (AlgebraicGeometry.Scheme.restrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))) | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y | |
| r))))).val.base).obj | |
| U)))).val.c | |
| (Opposite.op ⊤) =?= (?f ≫ ?g) ≫ ?h ▶ | |
| [Meta.check] [0.073804s] ✅ fun _a ↦ | |
| (CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict Y | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).val.c | |
| (Opposite.op ⊤) ≫ | |
| (CategoryTheory.NatTrans.app f.val.c | |
| (Opposite.op | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).obj | |
| ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.eqToHom | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((TopologicalSpace.Opens.map | |
| (f ∣_ AlgebraicGeometry.Scheme.basicOpen Y r).val.base).obj | |
| ⊤) = | |
| (TopologicalSpace.Opens.map f.val.base).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).obj | |
| ⊤))).op) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict | |
| (AlgebraicGeometry.Scheme.restrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))) | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y | |
| r))))).val.base).obj | |
| U)))).val.c | |
| (Opposite.op ⊤) = | |
| (CategoryTheory.NatTrans.app f.val.c (Opposite.op ⊤) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U))).val.c | |
| (Opposite.op ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.homOfLE | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen | |
| Y r))))).val.base).obj | |
| U)))).op.obj | |
| (Opposite.op ⊤)).unop ≤ | |
| (IsOpenMap.functor (_ : IsOpenMap ↑(TopologicalSpace.Opens.inclusion U))).obj | |
| (Opposite.op ⊤).unop)).op) = | |
| (CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict Y | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).val.c | |
| (Opposite.op ⊤) ≫ | |
| _a = | |
| (CategoryTheory.NatTrans.app f.val.c (Opposite.op ⊤) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U))).val.c | |
| (Opposite.op ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.homOfLE | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen | |
| Y r))))).val.base).obj | |
| U)))).op.obj | |
| (Opposite.op ⊤)).unop ≤ | |
| (IsOpenMap.functor (_ : IsOpenMap ↑(TopologicalSpace.Opens.inclusion U))).obj | |
| (Opposite.op ⊤).unop)).op) ▶ | |
| [Meta.isDefEq] [1.236472s] ✅ (CategoryTheory.NatTrans.app f.val.c (Opposite.op ⊤) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U))).val.c | |
| (Opposite.op ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.homOfLE | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y | |
| r))))).val.base).obj | |
| U)))).op.obj | |
| (Opposite.op ⊤)).unop ≤ | |
| (IsOpenMap.functor (_ : IsOpenMap ↑(TopologicalSpace.Opens.inclusion U))).obj | |
| (Opposite.op ⊤).unop)).op =?= (?f ≫ ?g) ≫ ?h ▶ | |
| [Meta.check] [0.086676s] ✅ fun _a ↦ | |
| (CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict Y | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).val.c | |
| (Opposite.op ⊤) ≫ | |
| CategoryTheory.NatTrans.app f.val.c | |
| (Opposite.op | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).obj | |
| ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.eqToHom | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((TopologicalSpace.Opens.map | |
| (f ∣_ AlgebraicGeometry.Scheme.basicOpen Y r).val.base).obj | |
| ⊤) = | |
| (TopologicalSpace.Opens.map f.val.base).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).obj | |
| ⊤))).op ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict | |
| (AlgebraicGeometry.Scheme.restrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))) | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y | |
| r))))).val.base).obj | |
| U)))).val.c | |
| (Opposite.op ⊤) = | |
| (CategoryTheory.NatTrans.app f.val.c (Opposite.op ⊤) ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U))).val.c | |
| (Opposite.op ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.homOfLE | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen | |
| Y r))))).val.base).obj | |
| U)))).op.obj | |
| (Opposite.op ⊤)).unop ≤ | |
| (IsOpenMap.functor (_ : IsOpenMap ↑(TopologicalSpace.Opens.inclusion U))).obj | |
| (Opposite.op ⊤).unop)).op) = | |
| (CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict Y | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).val.c | |
| (Opposite.op ⊤) ≫ | |
| CategoryTheory.NatTrans.app f.val.c | |
| (Opposite.op | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).obj | |
| ⊤)) ≫ | |
| X.presheaf.map | |
| (CategoryTheory.eqToHom | |
| (_ : | |
| (IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))).obj | |
| ((TopologicalSpace.Opens.map | |
| (f ∣_ AlgebraicGeometry.Scheme.basicOpen Y r).val.base).obj | |
| ⊤) = | |
| (TopologicalSpace.Opens.map f.val.base).obj | |
| ((IsOpenMap.functor | |
| (_ : | |
| IsOpenMap | |
| ↑(TopologicalSpace.Opens.inclusion | |
| (AlgebraicGeometry.Scheme.basicOpen Y r)))).obj | |
| ⊤))).op ≫ | |
| CategoryTheory.NatTrans.app | |
| (AlgebraicGeometry.Scheme.ofRestrict | |
| (AlgebraicGeometry.Scheme.restrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y r))))) | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map | |
| (AlgebraicGeometry.Scheme.ofRestrict X | |
| (_ : | |
| OpenEmbedding | |
| ↑(TopologicalSpace.Opens.inclusion | |
| ((TopologicalSpace.Opens.map f.val.base).obj | |
| (AlgebraicGeometry.Scheme.basicOpen Y | |
| r))))).val.base).obj | |
| U)))).val.c | |
| (Opposite.op ⊤) = | |
| _a) ▶ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment