Structures · Category theory
CategoryTheory.PreGaloisCategory.IsConnected
An object of a category C is connected if it is not initial
and has no non-trivial subobjects. Lenstra, 3.12.
- Defined in
- Mathlib.CategoryTheory.Galois.Basic
- Shape
- One type argument · adds notInitial, noTrivialComponent
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by35
- CategoryTheory.PreGaloisCategory.autMap
- CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected
- CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected
- CategoryTheory.PreGaloisCategory.autMapHom
- CategoryTheory.PreGaloisCategory.surjective_of_nonempty_fiber_of_isConnected
- CategoryTheory.PreGaloisCategory.IsConnected.noTrivialComponent
- CategoryTheory.PreGaloisCategory.comp_autMap
- CategoryTheory.PreGaloisCategory.exists_autMap
- CategoryTheory.PreGaloisCategory.comp_autMap_apply
- CategoryTheory.PreGaloisCategory.autMap_unique
- CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected
- CategoryTheory.PreGaloisCategory.quotientByAutTerminalEquivUniqueQuotient
- CategoryTheory.PreGaloisCategory.isGalois_iff_pretransitive
- CategoryTheory.FintypeCat.isoQuotientStabilizerOfIsConnected
- CategoryTheory.PreGaloisCategory.epi_of_nonempty_of_isConnected
- CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected
- CategoryTheory.PreGaloisCategory.connected_component_unique
- CategoryTheory.PreGaloisCategory.isGalois_iff_aux
- CategoryTheory.PreGaloisCategory.fiberIsoQuotientStabilizer
- CategoryTheory.PreGaloisCategory.PreservesIsConnected.preserves
- CategoryTheory.PreGaloisCategory.instFiniteAutOfIsConnected
- CategoryTheory.PreGaloisCategory.isPretransitive_of_surjective
- CategoryTheory.PreGaloisCategory.autMapHom_apply
- CategoryTheory.PreGaloisCategory.IsConnected.notInitial
- CategoryTheory.PreGaloisCategory.card_aut_le_card_fiber_of_connected
- CategoryTheory.PreGaloisCategory.autMapHom.congr_simp
- CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected
- CategoryTheory.PreGaloisCategory.card_hom_le_card_fiber_of_connected
- CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_connected
- CategoryTheory.PreGaloisCategory.instIsPretransitiveObjFiniteObjFintypeCatOfIsConnected
- CategoryTheory.PreGaloisCategory.instFiniteHomOfIsConnected
- CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isConnected
- CategoryTheory.PreGaloisCategory.autMap.congr_simp
- CategoryTheory.PreGaloisCategory.autMap_apply_mul
- CategoryTheory.PreGaloisCategory.autMap_comp
Ancestors0
No ancestors.