Final

📁 Source: Mathlib/CategoryTheory/Comma/Final.lean

Statistics

Metric	Count
Definitions	0
Theorems final_fst, final_snd, initial_fst, initial_snd, isCofiltered_of_initial, isConnected_comma_of_final, isConnected_comma_of_initial, isFiltered_of_final, map_final	9
Total	9

CategoryTheory.Comma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
final_fst 📖	mathematical	—	CategoryTheory.Functor.Final CategoryTheory.Comma CategoryTheory.commaCategory fst	—	CategoryTheory.Functor.final_comp CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Functor.final_of_natIso isEquivalenceMap CategoryTheory.Equivalence.faithful_functor CategoryTheory.Equivalence.full_functor CategoryTheory.Iso.isIso_hom
final_snd 📖	mathematical	—	CategoryTheory.Functor.Final CategoryTheory.Comma CategoryTheory.commaCategory snd	—	map_final CategoryTheory.Functor.final_of_isFiltered_of_pUnit CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Functor.isEquivalence_refl CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.final_of_natIso CategoryTheory.Functor.final_comp CategoryTheory.Equivalence.isEquivalence_functor
initial_fst 📖	mathematical	—	CategoryTheory.Functor.Initial CategoryTheory.Comma CategoryTheory.commaCategory fst	—	CategoryTheory.Functor.final_equivalence_comp CategoryTheory.Functor.instIsEquivalenceOppositeLeftOp CategoryTheory.Equivalence.isEquivalence_functor final_snd CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.Functor.final_op_of_initial CategoryTheory.Functor.final_of_natIso CategoryTheory.Functor.initial_of_final_op
initial_snd 📖	mathematical	—	CategoryTheory.Functor.Initial CategoryTheory.Comma CategoryTheory.commaCategory snd	—	CategoryTheory.Functor.final_equivalence_comp CategoryTheory.Functor.instIsEquivalenceOppositeLeftOp CategoryTheory.Equivalence.isEquivalence_functor final_fst CategoryTheory.Functor.final_op_of_initial CategoryTheory.Functor.final_of_natIso CategoryTheory.Functor.initial_of_final_op
isCofiltered_of_initial 📖	mathematical	—	CategoryTheory.IsCofiltered CategoryTheory.Comma CategoryTheory.commaCategory	—	CategoryTheory.IsCofiltered.of_equivalence CategoryTheory.isCofiltered_op_of_isFiltered isFiltered_of_final CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.Functor.final_op_of_initial
isConnected_comma_of_final 📖	mathematical	—	CategoryTheory.IsConnected CategoryTheory.Comma CategoryTheory.commaCategory	—	CategoryTheory.Functor.isConnected_iff_of_final final_fst
isConnected_comma_of_initial 📖	mathematical	—	CategoryTheory.IsConnected CategoryTheory.Comma CategoryTheory.commaCategory	—	CategoryTheory.Functor.isConnected_iff_of_initial initial_snd
isFiltered_of_final 📖	mathematical	—	CategoryTheory.IsFiltered CategoryTheory.Comma CategoryTheory.commaCategory	—	CategoryTheory.Functor.final_const_of_isTerminal CategoryTheory.instIsFilteredDiscretePUnit CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.IsFiltered.of_final map_final CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Functor.isEquivalence_refl CategoryTheory.Functor.final_iff_isFiltered_structuredArrow CategoryTheory.IsFiltered.toIsFilteredOrEmpty CategoryTheory.IsFiltered.of_equivalence CategoryTheory.isFiltered_of_representablyCoflat
map_final 📖	mathematical	—	CategoryTheory.Functor.Final CategoryTheory.Comma CategoryTheory.commaCategory map CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Iso.inv	—	CategoryTheory.Iso.isIso_inv CategoryTheory.isConnected_iff_of_equivalence CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.NatTrans.ext' CategoryTheory.Functor.whiskerRight_id' CategoryTheory.Functor.whiskerLeft_twice CategoryTheory.Category.assoc CategoryTheory.IsIso.Iso.inv_inv isConnected_comma_of_final CategoryTheory.Functor.Final.out CategoryTheory.Functor.final_of_natIso CategoryTheory.Functor.final_comp CategoryTheory.StructuredArrow.final_post CategoryTheory.StructuredArrow.final_map₂_id CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Functor.isEquivalence_refl CategoryTheory.Iso.isIso_hom CategoryTheory.StructuredArrow.final_pre

---

← Back to Index