Commit 2024-02-14 07:40 f148b92c

View on Github →

feat(CategoryTheory/Galois): decomposition in connected components (#10419) Shows that any object in a Galois category is the sum of its connected components. Also shows that the connected components are unique up to isomorphism.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/FintypeCat.lean

added theorem FintypeCat.hom_inv_id_apply

added theorem FintypeCat.inv_hom_id_apply

Modified Mathlib/CategoryTheory/Galois/Basic.lean

added theorem CategoryTheory.PreGaloisCategory.cardFiber_coprod_eq_sum

added theorem CategoryTheory.PreGaloisCategory.cardFiber_eq_of_iso

added theorem CategoryTheory.PreGaloisCategory.has_non_trivial_subobject_of_not_isConnected_of_not_initial

added theorem CategoryTheory.PreGaloisCategory.isIso_of_mono_of_eqCardFiber

added theorem CategoryTheory.PreGaloisCategory.ltCardFiber_of_mono_of_notIso

added theorem CategoryTheory.PreGaloisCategory.non_zero_card_fiber_of_not_initial

Created Mathlib/CategoryTheory/Galois/Decomposition.lean

added theorem CategoryTheory.PreGaloisCategory.connected_component_unique

added theorem CategoryTheory.PreGaloisCategory.fiber_in_connected_component

added theorem CategoryTheory.PreGaloisCategory.has_decomp_connected_components'

added theorem CategoryTheory.PreGaloisCategory.has_decomp_connected_components

Modified Mathlib/CategoryTheory/Limits/MonoCoprod.lean

added theorem CategoryTheory.Limits.MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono

Created Mathlib/CategoryTheory/Limits/Shapes/CombinedProducts.lean

added def CategoryTheory.Limits.Cofan.combPairIsColimit

added def CategoryTheory.Limits.Fan.combPairIsLimit

Modified Mathlib/CategoryTheory/Limits/Shapes/Types.lean

added theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst_apply

added theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd_apply