Commit 2024-02-08 20:07 7ab6771e

View on Github →

feat(CategoryTheory/Galois): characterisation of connected finite G-sets (#10228) A finite G-set is connected if and only if the G-action is transitive.

Estimated changes

Modified Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

added theorem CategoryTheory.ConcreteCategory.isIso_iff_bijective

Modified Mathlib/CategoryTheory/FintypeCat.lean

Modified Mathlib/CategoryTheory/Galois/Basic.lean

added theorem CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty

Modified Mathlib/CategoryTheory/Galois/Examples.lean

added theorem CategoryTheory.FintypeCat.Action.connected_iff_transitive

added theorem CategoryTheory.FintypeCat.Action.connected_of_transitive

added theorem CategoryTheory.FintypeCat.Action.pretransitive_of_connected

Modified Mathlib/CategoryTheory/Limits/FintypeCat.lean

Modified Mathlib/RepresentationTheory/Action/Concrete.lean