Representable

📁 Source: Mathlib/CategoryTheory/MorphismProperty/Representable.lean

Statistics

Metric	Count
Definitions relativelyRepresentable, fst, fst', lift', lift₃, pullback, pullback₃, p₁, p₂, p₃, π, snd, symmetry, symmetryIso, presheaf, relative	16
Theorems diag_iff, diag_of_map_from_obj, hom_ext, hom_ext', hom_ext'_iff, hom_ext_iff, instIsIsoSymmetryOfFaithful, isMultiplicative, isPullback, isPullback', isPullback_of_map, isStableUnderBaseChange, isomorphisms_le, lift'_fst, lift'_fst_assoc, lift'_snd, lift'_snd_assoc, lift_fst, lift_fst_assoc, lift_snd, lift_snd_assoc, lift₃_p₁, lift₃_p₁_assoc, lift₃_p₂, lift₃_p₂_assoc, lift₃_p₃, lift₃_p₃_assoc, map, map_fst', of_diag, of_isIso, fst_fst'_eq_p₁, fst_fst'_eq_p₁_assoc, fst_snd_eq_p₂, fst_snd_eq_p₂_assoc, hom_ext, hom_ext_iff, map_p₁_comp, map_p₁_comp_assoc, map_p₂_comp, map_p₂_comp_assoc, map_p₃_comp, map_p₃_comp_assoc, snd_fst'_eq_p₁, snd_fst'_eq_p₁_assoc, snd_snd_eq_p₃, snd_snd_eq_p₃_assoc, respectsIso, symmetryIso_hom, symmetryIso_inv, symmetry_fst, symmetry_fst_assoc, symmetry_snd, symmetry_snd_assoc, symmetry_symmetry, symmetry_symmetry_assoc, toPullbackTerminal, w, w', w'_assoc, w_assoc, fst'_self_eq_snd, isIso_fst'_self, of_relative_map, presheaf_mono_of_le, presheaf_monomorphisms_le_monomorphisms, of_exists, property, property_snd, rep, relative_isMultiplicative, relative_isStableUnderBaseChange, relative_isStableUnderComposition, relative_map, relative_map_iff, relative_monotone, relative_of_snd, relative_respectsIso	78
Total	94

CategoryTheory.Functor

Definitions

Name	Category	Theorems
relativelyRepresentable 📖	CompOp	9 math math: relativelyRepresentable.isStableUnderBaseChange, relativelyRepresentable.respectsIso, relativelyRepresentable.isomorphisms_le, relativelyRepresentable.isMultiplicative, relativelyRepresentable.map, relativelyRepresentable.diag_iff, relativelyRepresentable.of_isIso, relativelyRepresentable.toPullbackTerminal, CategoryTheory.MorphismProperty.relative.rep

CategoryTheory.Functor.relativelyRepresentable

Definitions

Name	Category	Theorems
fst 📖	CompOp	7 math math: lift_fst, hom_ext_iff, lift_fst_assoc, map_fst', isPullback, w_assoc, w
fst' 📖	CompOp	24 math math: pullback₃.snd_fst'_eq_p₁, CategoryTheory.MorphismProperty.isIso_fst'_self, pullback₃.snd_snd_eq_p₃_assoc, lift'_fst, CategoryTheory.MorphismProperty.fst'_self_eq_snd, map_fst', symmetry_fst, pullback₃.snd_snd_eq_p₃, w'_assoc, pullback₃.fst_snd_eq_p₂_assoc, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_f, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t', w', lift'_fst_assoc, symmetry_snd_assoc, symmetry_fst_assoc, pullback₃.fst_fst'_eq_p₁_assoc, hom_ext'_iff, pullback₃.fst_snd_eq_p₂, pullback₃.fst_fst'_eq_p₁, isPullback', pullback₃.snd_fst'_eq_p₁_assoc, symmetry_snd, isPullback_of_map
lift' 📖	CompOp	4 math math: lift'_fst, lift'_fst_assoc, lift'_snd_assoc, lift'_snd
lift₃ 📖	CompOp	7 math math: lift₃_p₁_assoc, lift₃_p₃, lift₃_p₁, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t', lift₃_p₂_assoc, lift₃_p₃_assoc, lift₃_p₂
pullback 📖	CompOp	39 math math: pullback₃.snd_fst'_eq_p₁, lift_fst, CategoryTheory.MorphismProperty.isIso_fst'_self, symmetry_symmetry, pullback₃.snd_snd_eq_p₃_assoc, lift'_fst, lift_snd, CategoryTheory.MorphismProperty.relative.property_snd, hom_ext_iff, lift_snd_assoc, symmetryIso_hom, lift_fst_assoc, map_fst', symmetry_symmetry_assoc, symmetry_fst, isPullback, pullback₃.snd_snd_eq_p₃, w'_assoc, pullback₃.fst_snd_eq_p₂_assoc, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_V, w_assoc, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t', w', lift'_fst_assoc, instIsIsoSymmetryOfFaithful, symmetry_snd_assoc, symmetry_fst_assoc, pullback₃.fst_fst'_eq_p₁_assoc, hom_ext'_iff, pullback₃.fst_snd_eq_p₂, pullback₃.fst_fst'_eq_p₁, symmetryIso_inv, w, isPullback', pullback₃.snd_fst'_eq_p₁_assoc, symmetry_snd, lift'_snd_assoc, isPullback_of_map, lift'_snd
pullback₃ 📖	CompOp	13 math math: pullback₃.map_p₃_comp, lift₃_p₁_assoc, pullback₃.map_p₁_comp, lift₃_p₃, lift₃_p₁, pullback₃.map_p₁_comp_assoc, pullback₃.hom_ext_iff, pullback₃.map_p₂_comp_assoc, pullback₃.map_p₂_comp, lift₃_p₂_assoc, pullback₃.map_p₃_comp_assoc, lift₃_p₃_assoc, lift₃_p₂
snd 📖	CompOp	23 math math: pullback₃.snd_snd_eq_p₃_assoc, lift_snd, CategoryTheory.MorphismProperty.relative.property_snd, hom_ext_iff, lift_snd_assoc, CategoryTheory.MorphismProperty.fst'_self_eq_snd, symmetry_fst, isPullback, pullback₃.snd_snd_eq_p₃, w'_assoc, pullback₃.fst_snd_eq_p₂_assoc, w_assoc, w', symmetry_snd_assoc, symmetry_fst_assoc, hom_ext'_iff, pullback₃.fst_snd_eq_p₂, w, isPullback', symmetry_snd, lift'_snd_assoc, isPullback_of_map, lift'_snd
symmetry 📖	CompOp	10 math math: symmetry_symmetry, symmetryIso_hom, symmetry_symmetry_assoc, symmetry_fst, instIsIsoSymmetryOfFaithful, symmetry_snd_assoc, symmetry_fst_assoc, symmetryIso_inv, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t, symmetry_snd
symmetryIso 📖	CompOp	2 math math: symmetryIso_hom, symmetryIso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diag_iff 📖	mathematical	—	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.diag CategoryTheory.Functor.obj	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape of_diag diag_of_map_from_obj
diag_of_map_from_obj 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.diag	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.prod.hom_ext CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.assoc prodIsoPullback_inv_fst prodIsoPullback_inv_snd CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.comp_id CategoryTheory.IsPullback.of_iso_pullback CategoryTheory.Limits.pullback.condition CategoryTheory.CommSq.w CategoryTheory.Limits.terminal.comp_from toPullbackTerminal CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Category.id_comp CategoryTheory.IsPullback.toCommSq CategoryTheory.IsPullback.flip CategoryTheory.Functor.map_preimage CategoryTheory.IsPullback.of_isLimit CategoryTheory.IsPullback.isLimit' CategoryTheory.MorphismProperty.RespectsRight.postcomp CategoryTheory.MorphismProperty.Respects.toRespectsRight respectsIso CategoryTheory.Iso.isIso_inv
hom_ext 📖	—	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj pullback CategoryTheory.Functor.map fst snd	—	—	CategoryTheory.Functor.map_injective CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext isPullback CategoryTheory.Functor.map_comp CategoryTheory.Functor.congr_map
hom_ext' 📖	—	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback fst' snd	—	—	hom_ext CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_preimage CategoryTheory.Functor.congr_map
hom_ext'_iff 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback fst' snd	—	hom_ext'
hom_ext_iff 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj pullback CategoryTheory.Functor.map fst snd	—	hom_ext
instIsIsoSymmetryOfFaithful 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.IsIso pullback symmetry	—	CategoryTheory.Iso.isIso_hom
isMultiplicative 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.Functor.relativelyRepresentable	—	of_isIso CategoryTheory.IsIso.id CategoryTheory.Functor.map_comp CategoryTheory.IsPullback.paste_vert isPullback
isPullback 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable	CategoryTheory.IsPullback CategoryTheory.Functor.obj pullback fst CategoryTheory.Functor.map snd	—	—
isPullback' 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.IsPullback pullback CategoryTheory.Functor.map fst' snd	—	isPullback map_fst'
isPullback_of_map 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.IsPullback pullback fst' snd	—	CategoryTheory.IsPullback.of_map CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits w' isPullback'
isStableUnderBaseChange 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange CategoryTheory.Functor.relativelyRepresentable	—	CategoryTheory.Category.assoc w CategoryTheory.IsPullback.of_right' isPullback
isomorphisms_le 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.isomorphisms CategoryTheory.Functor.relativelyRepresentable	—	of_isIso
lift'_fst 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	pullback lift' fst'	—	CategoryTheory.Functor.map_injective CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_preimage lift_fst
lift'_fst_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	pullback lift' fst'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift'_fst
lift'_snd 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	pullback lift' snd	—	lift_snd
lift'_snd_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	pullback lift' snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift'_snd
lift_fst 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	pullback lift fst	—	isPullback CategoryTheory.Functor.map_preimage CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst
lift_fst_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	pullback lift fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_fst
lift_snd 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	pullback lift snd	—	CategoryTheory.Functor.map_injective isPullback CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_preimage CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd
lift_snd_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	pullback lift snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_snd
lift₃_p₁ 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	pullback₃ lift₃ pullback₃.p₁	—	CategoryTheory.Limits.limit.lift_π_assoc lift'_fst
lift₃_p₁_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	pullback₃ lift₃ pullback₃.p₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift₃_p₁
lift₃_p₂ 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	pullback₃ lift₃ pullback₃.p₂	—	CategoryTheory.Limits.limit.lift_π_assoc lift'_snd
lift₃_p₂_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	pullback₃ lift₃ pullback₃.p₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift₃_p₂
lift₃_p₃ 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	pullback₃ lift₃ pullback₃.p₃	—	CategoryTheory.Limits.limit.lift_π_assoc lift'_snd
lift₃_p₃_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	pullback₃ lift₃ pullback₃.p₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift₃_p₃
map 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Functor.map_surjective CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.map_isPullback CategoryTheory.IsPullback.of_hasPullback
map_fst' 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.Functor.map pullback fst' fst	—	CategoryTheory.Functor.map_preimage
of_diag 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.diag	CategoryTheory.Functor.obj	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Limits.pullback_map_diagonal_isPullback CategoryTheory.CommSq.w CategoryTheory.Limits.instHasLimitCompOfPreservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.prod.hom_ext CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.assoc prodIsoPullback_inv_fst prodIsoPullback_inv_snd CategoryTheory.IsPullback.toCommSq CategoryTheory.Limits.terminal.comp_from CategoryTheory.IsPullback.of_vert_isIso_mono CategoryTheory.Iso.isIso_hom CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Limits.prod.map_fst prodIsoPullback_inv_fst_assoc CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.prod.map_snd prodIsoPullback_inv_snd_assoc CategoryTheory.IsPullback.isLimit' CategoryTheory.IsPullback.of_iso_pullback CategoryTheory.Limits.pullback.condition CategoryTheory.Functor.map_preimage
of_isIso 📖	mathematical	—	CategoryTheory.Functor.relativelyRepresentable	—	CategoryTheory.IsPullback.of_vert_isIso CategoryTheory.Functor.map_isIso CategoryTheory.IsIso.id CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
respectsIso 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso CategoryTheory.Functor.relativelyRepresentable	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso isStableUnderBaseChange
symmetryIso_hom 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.Iso.hom pullback symmetryIso symmetry	—	—
symmetryIso_inv 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.Iso.inv pullback symmetryIso symmetry	—	—
symmetry_fst 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback symmetry fst' snd	—	lift'_fst
symmetry_fst_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback symmetry fst' snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' symmetry_fst
symmetry_snd 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback symmetry snd fst'	—	lift'_snd
symmetry_snd_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback symmetry snd fst'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' symmetry_snd
symmetry_symmetry 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback symmetry CategoryTheory.CategoryStruct.id	—	hom_ext' CategoryTheory.Category.assoc symmetry_fst symmetry_snd CategoryTheory.Category.id_comp
symmetry_symmetry_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback symmetry	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' symmetry_symmetry
toPullbackTerminal 📖	mathematical	—	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.Limits.pullback CategoryTheory.Limits.terminal CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.terminal.from CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.lift CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.terminal.comp_from CategoryTheory.Limits.instHasLimitCompOfPreservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.assoc CategoryTheory.MorphismProperty.RespectsRight.postcomp CategoryTheory.MorphismProperty.Respects.toRespectsRight respectsIso CategoryTheory.Iso.isIso_inv map CategoryTheory.Functor.map_preimage
w 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj pullback fst CategoryTheory.Functor.map snd	—	CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq isPullback
w' 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback fst' snd	—	CategoryTheory.Functor.map_injective CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_preimage w
w'_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback fst' snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w'
w_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj pullback fst CategoryTheory.Functor.map snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w

CategoryTheory.Functor.relativelyRepresentable.pullback₃

Definitions

Name	Category	Theorems
p₁ 📖	CompOp	10 math math: snd_fst'_eq_p₁, CategoryTheory.Functor.relativelyRepresentable.lift₃_p₁_assoc, map_p₁_comp, CategoryTheory.Functor.relativelyRepresentable.lift₃_p₁, map_p₁_comp_assoc, hom_ext_iff, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t', fst_fst'_eq_p₁_assoc, fst_fst'_eq_p₁, snd_fst'_eq_p₁_assoc
p₂ 📖	CompOp	8 math math: hom_ext_iff, fst_snd_eq_p₂_assoc, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t', map_p₂_comp_assoc, map_p₂_comp, CategoryTheory.Functor.relativelyRepresentable.lift₃_p₂_assoc, fst_snd_eq_p₂, CategoryTheory.Functor.relativelyRepresentable.lift₃_p₂
p₃ 📖	CompOp	8 math math: map_p₃_comp, snd_snd_eq_p₃_assoc, CategoryTheory.Functor.relativelyRepresentable.lift₃_p₃, snd_snd_eq_p₃, hom_ext_iff, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t', map_p₃_comp_assoc, CategoryTheory.Functor.relativelyRepresentable.lift₃_p₃_assoc
π 📖	CompOp	6 math math: map_p₃_comp, map_p₁_comp, map_p₁_comp_assoc, map_p₂_comp_assoc, map_p₂_comp, map_p₃_comp_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fst_fst'_eq_p₁ 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Functor.relativelyRepresentable.pullback CategoryTheory.Functor.relativelyRepresentable.fst' CategoryTheory.Limits.pullback.fst p₁	—	—
fst_fst'_eq_p₁_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Functor.relativelyRepresentable.pullback CategoryTheory.Functor.relativelyRepresentable.fst' CategoryTheory.Limits.pullback.fst p₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fst_fst'_eq_p₁
fst_snd_eq_p₂ 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Functor.relativelyRepresentable.pullback CategoryTheory.Functor.relativelyRepresentable.fst' CategoryTheory.Limits.pullback.fst CategoryTheory.Functor.relativelyRepresentable.snd p₂	—	—
fst_snd_eq_p₂_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Functor.relativelyRepresentable.pullback CategoryTheory.Functor.relativelyRepresentable.fst' CategoryTheory.Limits.pullback.fst CategoryTheory.Functor.relativelyRepresentable.snd p₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fst_snd_eq_p₂
hom_ext 📖	—	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.relativelyRepresentable.pullback₃ p₁ p₂ p₃	—	—	CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Functor.relativelyRepresentable.hom_ext' CategoryTheory.Category.assoc snd_fst'_eq_p₁
hom_ext_iff 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.relativelyRepresentable.pullback₃ p₁ p₂ p₃	—	hom_ext
map_p₁_comp 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.relativelyRepresentable.pullback₃ CategoryTheory.Functor.map p₁ π	—	—
map_p₁_comp_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.relativelyRepresentable.pullback₃ CategoryTheory.Functor.map p₁ π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_p₁_comp
map_p₂_comp 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.relativelyRepresentable.pullback₃ CategoryTheory.Functor.map p₂ π	—	CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Functor.relativelyRepresentable.w CategoryTheory.Functor.map_preimage
map_p₂_comp_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.relativelyRepresentable.pullback₃ CategoryTheory.Functor.map p₂ π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_p₂_comp
map_p₃_comp 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.relativelyRepresentable.pullback₃ CategoryTheory.Functor.map p₃ π	—	CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Functor.relativelyRepresentable.w CategoryTheory.Limits.pullback.condition CategoryTheory.Functor.map_preimage
map_p₃_comp_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.relativelyRepresentable.pullback₃ CategoryTheory.Functor.map p₃ π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_p₃_comp
snd_fst'_eq_p₁ 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Functor.relativelyRepresentable.pullback CategoryTheory.Functor.relativelyRepresentable.fst' CategoryTheory.Limits.pullback.snd p₁	—	CategoryTheory.Limits.pullback.condition
snd_fst'_eq_p₁_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Functor.relativelyRepresentable.pullback CategoryTheory.Functor.relativelyRepresentable.fst' CategoryTheory.Limits.pullback.snd p₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' snd_fst'_eq_p₁
snd_snd_eq_p₃ 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Functor.relativelyRepresentable.pullback CategoryTheory.Functor.relativelyRepresentable.fst' CategoryTheory.Limits.pullback.snd CategoryTheory.Functor.relativelyRepresentable.snd p₃	—	—
snd_snd_eq_p₃_assoc 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Functor.relativelyRepresentable.pullback CategoryTheory.Functor.relativelyRepresentable.fst' CategoryTheory.Limits.pullback.snd CategoryTheory.Functor.relativelyRepresentable.snd p₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' snd_snd_eq_p₃

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
presheaf 📖	CompOp	1 math math: presheaf_monomorphisms_le_monomorphisms
relative 📖	CompOp	9 math math: relative_respectsIso, relative_isStableUnderBaseChange, relative_isStableUnderComposition, relative_map_iff, relative_map, relative_monotone, relative.of_exists, relative_isMultiplicative, relative_of_snd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fst'_self_eq_snd 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra monomorphisms presheaf CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda	CategoryTheory.Functor.relativelyRepresentable.fst' relative.rep CategoryTheory.Yoneda.yoneda_full CategoryTheory.Functor.relativelyRepresentable.snd	—	presheaf_mono_of_le CategoryTheory.Functor.map_injective relative.rep CategoryTheory.Yoneda.yoneda_faithful CategoryTheory.Yoneda.yoneda_full CategoryTheory.cancel_mono CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.Functor.relativelyRepresentable.isPullback'
isIso_fst'_self 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra monomorphisms presheaf CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda	CategoryTheory.IsIso CategoryTheory.Functor.relativelyRepresentable.pullback relative.rep CategoryTheory.Functor.relativelyRepresentable.fst' CategoryTheory.Yoneda.yoneda_full	—	presheaf_mono_of_le relative.rep CategoryTheory.Yoneda.yoneda_full CategoryTheory.IsPullback.isIso_fst_of_mono CategoryTheory.Functor.relativelyRepresentable.isPullback' CategoryTheory.Functor.FullyFaithful.isIso_of_isIso_map
of_relative_map 📖	—	relative CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—	relative.property CategoryTheory.IsPullback.id_horiz
presheaf_mono_of_le 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra monomorphisms presheaf CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda	CategoryTheory.Mono	—	presheaf_monomorphisms_le_monomorphisms relative_monotone
presheaf_monomorphisms_le_monomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra presheaf monomorphisms	—	relative.rep CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Yoneda.yoneda_full relative.property_snd CategoryTheory.cancel_mono CategoryTheory.Functor.relativelyRepresentable.lift_snd CategoryTheory.Yoneda.yoneda_faithful CategoryTheory.Functor.relativelyRepresentable.lift_fst CategoryTheory.eq_whisker CategoryTheory.Functor.congr_map CategoryTheory.hom_ext_yoneda CategoryTheory.Category.assoc
relative_isMultiplicative 📖	mathematical	—	IsMultiplicative relative	—	relative.of_exists CategoryTheory.Functor.map_id CategoryTheory.IsPullback.of_id_snd id_mem IsMultiplicative.toContainsIdentities relative_isStableUnderComposition IsMultiplicative.toIsStableUnderComposition
relative_isStableUnderBaseChange 📖	mathematical	—	IsStableUnderBaseChange relative	—	of_isPullback CategoryTheory.Functor.relativelyRepresentable.isStableUnderBaseChange relative.rep relative.property CategoryTheory.IsPullback.paste_horiz
relative_isStableUnderComposition 📖	mathematical	—	IsStableUnderComposition relative	—	comp_mem IsMultiplicative.toIsStableUnderComposition CategoryTheory.Functor.relativelyRepresentable.isMultiplicative CategoryTheory.Category.assoc CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.Functor.relativelyRepresentable.lift_snd relative.property CategoryTheory.IsPullback.of_bot CategoryTheory.Functor.map_comp CategoryTheory.Functor.relativelyRepresentable.lift_fst CategoryTheory.Functor.relativelyRepresentable.isPullback relative.property_snd
relative_map 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan	relative CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	relative.of_exists IsStableUnderBaseChange.respectsIso CategoryTheory.Functor.map_surjective CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.IsPullback.map CategoryTheory.IsPullback.of_hasPullback pullback_snd instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange
relative_map_iff 📖	mathematical	—	relative CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	of_relative_map relative_map CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit
relative_monotone 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra	relative	—	relative.rep relative.property
relative_of_snd 📖	mathematical	CategoryTheory.Functor.relativelyRepresentable CategoryTheory.Functor.relativelyRepresentable.pullback CategoryTheory.Functor.relativelyRepresentable.snd	relative	—	relative.of_exists CategoryTheory.Functor.relativelyRepresentable.isPullback
relative_respectsIso 📖	mathematical	—	RespectsIso relative	—	IsStableUnderBaseChange.respectsIso relative_isStableUnderBaseChange

CategoryTheory.MorphismProperty.relative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_exists 📖	mathematical	—	CategoryTheory.MorphismProperty.relative	—	CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.Functor.map_injective CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_preimage CategoryTheory.IsPullback.isoIsPullback_hom_snd CategoryTheory.Category.comp_id
property 📖	—	CategoryTheory.MorphismProperty.relative CategoryTheory.IsPullback CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—	—
property_snd 📖	mathematical	CategoryTheory.MorphismProperty.relative	CategoryTheory.Functor.relativelyRepresentable.pullback rep CategoryTheory.Functor.relativelyRepresentable.snd	—	property rep CategoryTheory.Functor.relativelyRepresentable.isPullback
rep 📖	mathematical	CategoryTheory.MorphismProperty.relative	CategoryTheory.Functor.relativelyRepresentable	—	—

---

← Back to Index