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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.GlueData.J 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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.GlueData.U 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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.GlueData.V AlgebraicGeometry.Scheme.GlueData.toGlueData glueData CategoryTheory.Functor.relativelyRepresentable.pullback	—	—
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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.GlueData.f AlgebraicGeometry.Scheme.GlueData.toGlueData glueData CategoryTheory.Functor.relativelyRepresentable.fst' 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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme.GlueData.glued glueData CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage 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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.GlueData.t AlgebraicGeometry.Scheme.GlueData.toGlueData glueData CategoryTheory.Functor.relativelyRepresentable.symmetry 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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.GlueData.t' AlgebraicGeometry.Scheme.GlueData.toGlueData glueData CategoryTheory.Functor.relativelyRepresentable.lift₃ CategoryTheory.Yoneda.yoneda_full CategoryTheory.Yoneda.yoneda_faithful CategoryTheory.Limits.pullback CategoryTheory.Functor.relativelyRepresentable.pullback 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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.IsIso CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.Sheaf.IsLocallyInjective Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.Sheaf.IsLocallySurjective Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	AlgebraicGeometry.Scheme.GlueData.glued glueData toGlued	—	AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion
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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.Functor.IsRepresentable	—	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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.NatTrans.app CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.GrothendieckTopology.yoneda AlgebraicGeometry.Scheme.subcanonical_zariskiTopology AlgebraicGeometry.Scheme.GlueData.glued glueData CategoryTheory.Sheaf.Hom.val 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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.NatTrans.app CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.GrothendieckTopology.yoneda AlgebraicGeometry.Scheme.subcanonical_zariskiTopology AlgebraicGeometry.Scheme.GlueData.glued glueData CategoryTheory.Sheaf.Hom.val yonedaGluedToSheaf Opposite.op toGlued DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct 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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.GlueData.glued glueData CategoryTheory.Functor.map toGlued CategoryTheory.Sheaf.Hom.val CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.val AlgebraicGeometry.Scheme.zariskiTopology	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.GlueData.glued glueData CategoryTheory.Functor.map toGlued CategoryTheory.Sheaf.Hom.val CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf 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