Commit 2024-02-01 20:02 ad46cc4e

View on Github →

feat(CategoryTheory/Galois): evaluation is injective and more basic properties (#9841) Shows one of the key technical lemmas about Galois categories, namely that evaluation on a point of the fibre of morphisms out of a connected object is injective. Also adds some more basic properties on when objects are initial and preservation and reflection of monomorphisms.

Estimated changes

Modified Mathlib/CategoryTheory/Galois/Basic.lean

added theorem CategoryTheory.PreGaloisCategory.evaluationInjective_of_connected

added theorem CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_connected

added theorem CategoryTheory.PreGaloisCategory.initial_iff_fibre_empty

added theorem CategoryTheory.PreGaloisCategory.nonempty_fibre_of_connected

added theorem CategoryTheory.PreGaloisCategory.not_initial_of_inhabited

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean

added def CategoryTheory.Limits.IsInitial.isInitialIffObj

added def CategoryTheory.Limits.IsTerminal.isTerminalIffObj

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

added theorem CategoryTheory.Limits.Concrete.empty_of_initial_of_preserves

added theorem CategoryTheory.Limits.Concrete.initial_iff_empty_of_preserves_of_reflects

added theorem CategoryTheory.Limits.Concrete.initial_of_empty_of_reflects

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

added theorem CategoryTheory.Limits.Types.initial_iff_empty