Connected objects are invariant under equivalence

CategoryTheory.PreGaloisCategory.IsConnected is defined by conditions on initial objects, monomorphisms and isomorphisms alone, and an equivalence of categories preserves and reflects all three. This file records the resulting transport statements: connectedness is invariant under isomorphism inside a category, and an equivalence F : C ⥤ D makes F.obj A connected exactly when A is.

None of this needs the Galois axioms. Mathlib states connectedness for an object of an arbitrary category and only later restricts to PreGaloisCategory, and that arbitrary generality is what is used here; in particular the statements apply to a category that is merely equivalent to a Galois category, which is how a connectedness criterion is transported to a concrete category whose objects are not finite sets.

Main declarations

• TauCeti.isConnected_of_iso: an object isomorphic to a connected object is connected.
• TauCeti.isConnected_map: an equivalence carries connected objects to connected objects.
• TauCeti.isConnected_map_iff: connectedness of F.obj A is equivalent to connectedness of A.

theorem TauCeti.isConnected_of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} (e : A ≅ B) [CategoryTheory.PreGaloisCategory.IsConnected A] : CategoryTheory.PreGaloisCategory.IsConnected B

An object isomorphic to a connected object is connected.

theorem TauCeti.isConnected_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (A : C) [CategoryTheory.PreGaloisCategory.IsConnected A] : CategoryTheory.PreGaloisCategory.IsConnected (F.obj A)

An equivalence of categories carries connected objects to connected objects.

@[simp]

theorem TauCeti.isConnected_map_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (A : C) : CategoryTheory.PreGaloisCategory.IsConnected (F.obj A) ↔ CategoryTheory.PreGaloisCategory.IsConnected A

Connectedness transports along an equivalence of categories: for an equivalence F : C ⥤ D, an object A of C is connected exactly when F.obj A is.