Documentation Verification Report

Representability

📁 Source: Mathlib/AlgebraicGeometry/Sites/Representability.lean

Statistics

Metric	Count
Definitions `glueData`, `representableBy`, `toGlued`, `yonedaGluedToSheaf`, `yonedaIsoSheaf`	5
Theorems `comp_toGlued_eq`, `glueData_J`, `glueData_U`, `glueData_V`, `glueData_f`, `glueData_openCover_map`, `glueData_t`, `glueData_t'`, `instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf`, `instIsLocallyInjectiveHomYonedaGluedToSheaf`, `instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType`, `instIsOpenImmersionToGlued`, `isRepresentable`, `yonedaGluedToSheaf_app_comp`, `yonedaGluedToSheaf_app_toGlued`, `yoneda_toGlued_yonedaGluedToSheaf`, `yoneda_toGlued_yonedaGluedToSheaf_assoc`	17
Total	22

AlgebraicGeometry.Scheme.LocalRepresentability

Definitions

Name	Category	Theorems
`glueData` 📖	CompOp	16 math math: `instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType`, `comp_toGlued_eq`, `glueData_openCover_map`, `yoneda_toGlued_yonedaGluedToSheaf_assoc`, `glueData_V`, `instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf`, `glueData_f`, `glueData_t'`, `yoneda_toGlued_yonedaGluedToSheaf`, `instIsLocallyInjectiveHomYonedaGluedToSheaf`, `instIsOpenImmersionToGlued`, `yonedaGluedToSheaf_app_comp`, `glueData_J`, `glueData_t`, `glueData_U`, `yonedaGluedToSheaf_app_toGlued`
`representableBy` 📖	CompOp	—
`toGlued` 📖	CompOp	6 math math: `comp_toGlued_eq`, `glueData_openCover_map`, `yoneda_toGlued_yonedaGluedToSheaf_assoc`, `yoneda_toGlued_yonedaGluedToSheaf`, `instIsOpenImmersionToGlued`, `yonedaGluedToSheaf_app_toGlued`
`yonedaGluedToSheaf` 📖	CompOp	7 math math: `instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType`, `yoneda_toGlued_yonedaGluedToSheaf_assoc`, `instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf`, `yoneda_toGlued_yonedaGluedToSheaf`, `instIsLocallyInjectiveHomYonedaGluedToSheaf`, `yonedaGluedToSheaf_app_comp`, `yonedaGluedToSheaf_app_toGlued`
`yonedaIsoSheaf` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_toGlued_eq` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map`	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.GlueData.glued` `glueData` `toGlued`	—	`CategoryTheory.MorphismProperty.relative.rep` `CategoryTheory.Yoneda.yoneda_full` `CategoryTheory.Functor.relativelyRepresentable.lift'_fst` `CategoryTheory.Yoneda.yoneda_faithful` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.relativelyRepresentable.lift'_snd` `AlgebraicGeometry.Scheme.GlueData.glue_condition` `CategoryTheory.Functor.relativelyRepresentable.symmetry_fst_assoc`
`glueData_J` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.GlueData.J` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.GlueData.toGlueData` `glueData`	—	—
`glueData_U` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.GlueData.U` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.GlueData.toGlueData` `glueData`	—	—
`glueData_V` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.GlueData.V` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.GlueData.toGlueData` `glueData` `CategoryTheory.Functor.relativelyRepresentable.pullback` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.Functor.obj` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	—	—
`glueData_f` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.GlueData.f` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.GlueData.toGlueData` `glueData` `CategoryTheory.Functor.relativelyRepresentable.fst'` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology` `CategoryTheory.Yoneda.yoneda_full`	—	—
`glueData_openCover_map` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.GlueData.glued` `glueData` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `AlgebraicGeometry.IsOpenImmersion` `AlgebraicGeometry.Scheme.GlueData.openCover` `toGlued`	—	—
`glueData_t` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.GlueData.t` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.GlueData.toGlueData` `glueData` `CategoryTheory.Functor.relativelyRepresentable.symmetry` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology` `CategoryTheory.Yoneda.yoneda_full`	—	—
`glueData_t'` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.GlueData.t'` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.GlueData.toGlueData` `glueData` `CategoryTheory.Functor.relativelyRepresentable.lift₃` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.Yoneda.yoneda_full` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology` `CategoryTheory.Yoneda.yoneda_faithful` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.relativelyRepresentable.pullback` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.relativelyRepresentable.fst'` `CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂` `CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃` `CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁`	—	`CategoryTheory.Yoneda.yoneda_full`
`instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.IsIso` `CategoryTheory.Sheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.zariskiTopology` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.GrothendieckTopology.yoneda` `AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `AlgebraicGeometry.Scheme.GlueData.glued` `glueData` `yonedaGluedToSheaf`	—	`CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.Types.hasColimit` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `UnivLE.self` `AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `CategoryTheory.Sheaf.isLocallyBijective_iff_isIso` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.Functor.corepresentable_preservesLimit` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `instIsLocallyInjectiveHomYonedaGluedToSheaf` `instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType`
`instIsLocallyInjectiveHomYonedaGluedToSheaf` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.Sheaf.IsLocallyInjective` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.types` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Types.instFunLike` `CategoryTheory.Types.instConcreteCategory` `AlgebraicGeometry.Scheme.zariskiTopology` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.GrothendieckTopology.yoneda` `AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `AlgebraicGeometry.Scheme.GlueData.glued` `glueData` `yonedaGluedToSheaf`	—	`AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology` `CategoryTheory.GrothendieckTopology.superset_covering` `yonedaGluedToSheaf_app_comp` `comp_toGlued_eq` `yonedaGluedToSheaf_app_toGlued` `CategoryTheory.yonedaEquiv_naturality` `EquivLike.toEmbeddingLike` `CategoryTheory.GrothendieckTopology.intersection_covering` `CategoryTheory.GrothendieckTopology.pullback_stable`
`instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.Sheaf.IsLocallySurjective` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.zariskiTopology` `CategoryTheory.types` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Types.instFunLike` `CategoryTheory.Types.instConcreteCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.GrothendieckTopology.yoneda` `AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `AlgebraicGeometry.Scheme.GlueData.glued` `glueData` `yonedaGluedToSheaf`	—	`CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.Types.hasColimit` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `UnivLE.self` `CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_fac` `AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `CategoryTheory.Limits.Sigma.hom_ext` `CategoryTheory.NatTrans.ext'` `CategoryTheory.types_ext` `CategoryTheory.Limits.colimit.ι_desc_assoc` `yoneda_toGlued_yonedaGluedToSheaf` `CategoryTheory.Limits.colimit.ι_desc`
`instIsOpenImmersionToGlued` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`AlgebraicGeometry.IsOpenImmersion` `AlgebraicGeometry.Scheme.GlueData.glued` `glueData` `toGlued`	—	—
`isRepresentable` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.Functor.IsRepresentable` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	—	`CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.Types.hasColimit` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `UnivLE.self`
`yonedaGluedToSheaf_app_comp` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.NatTrans.app` `Opposite` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.opposite` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.GrothendieckTopology.yoneda` `AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `AlgebraicGeometry.Scheme.GlueData.glued` `glueData` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `yonedaGluedToSheaf` `Opposite.op` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	`AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `CategoryTheory.NatTrans.naturality`
`yonedaGluedToSheaf_app_toGlued` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.NatTrans.app` `Opposite` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.opposite` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.GrothendieckTopology.yoneda` `AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `AlgebraicGeometry.Scheme.GlueData.glued` `glueData` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `yonedaGluedToSheaf` `Opposite.op` `toGlued` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.yoneda` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.yonedaEquiv`	—	`AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `yoneda_toGlued_yonedaGluedToSheaf` `CategoryTheory.yonedaEquiv_comp` `CategoryTheory.yonedaEquiv_yoneda_map`
`yoneda_toGlued_yonedaGluedToSheaf` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `Opposite` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.opposite` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.yoneda` `AlgebraicGeometry.Scheme.GlueData.glued` `glueData` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology` `CategoryTheory.Functor.map` `toGlued` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.GrothendieckTopology.yoneda` `AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `yonedaGluedToSheaf`	—	`Equiv.injective` `AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `yonedaGluedToSheaf.eq_1` `CategoryTheory.yonedaEquiv_apply` `CategoryTheory.FunctorToTypes.comp` `CategoryTheory.yoneda_map_app` `CategoryTheory.Category.id_comp` `CategoryTheory.yonedaEquiv_symm_app_apply` `AlgebraicGeometry.Scheme.GlueData.sheafValGluedMk_val`
`yoneda_toGlued_yonedaGluedToSheaf_assoc` 📖	mathematical	`CategoryTheory.MorphismProperty.presheaf` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `Opposite` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.opposite` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.yoneda` `AlgebraicGeometry.Scheme.GlueData.glued` `glueData` `CategoryTheory.Functor.map` `toGlued` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `AlgebraicGeometry.Scheme.zariskiTopology` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.GrothendieckTopology.yoneda` `AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `yonedaGluedToSheaf`	—	`AlgebraicGeometry.Scheme.subcanonical_zariskiTopology` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `yoneda_toGlued_yonedaGluedToSheaf`

---

← Back to Index