Commit 2024-02-09 04:56 2e153a63

View on Github →

chore(CategoryTheory/Galois): fix spelling and rename connected objects (#10363) Changes the spelling of FibreFunctor to FiberFunctor to match the US spelling and adapts other names accordingly. Renames ConnectedObject to IsConnected to match IsGalois.

Estimated changes

Modified Mathlib/CategoryTheory/Galois/Basic.lean

deleted theorem CategoryTheory.PreGaloisCategory.evaluationInjective_of_connected

added theorem CategoryTheory.PreGaloisCategory.evaluationInjective_of_isConnected

deleted theorem CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_connected

added theorem CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected

added theorem CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty

deleted theorem CategoryTheory.PreGaloisCategory.initial_iff_fibre_empty

Modified Mathlib/CategoryTheory/Galois/Examples.lean

deleted theorem CategoryTheory.FintypeCat.Action.connected_iff_transitive

deleted theorem CategoryTheory.FintypeCat.Action.connected_of_transitive

added theorem CategoryTheory.FintypeCat.Action.isConnected_iff_transitive

added theorem CategoryTheory.FintypeCat.Action.isConnected_of_transitive

deleted theorem CategoryTheory.FintypeCat.Action.pretransitive_of_connected

added theorem CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected

Modified Mathlib/CategoryTheory/Galois/GaloisObjects.lean

modified theorem CategoryTheory.PreGaloisCategory.isGalois_iff_aux

modified theorem CategoryTheory.PreGaloisCategory.isGalois_iff_pretransitive