map_inversetheoremProved here from basic factsNo axioms
map_inverseLean 4Proved here from basic factsFormally verified
/-- **Functors carry inverse pairs to inverse pairs.** If `g` is a two-sided inverse of `f`,then `F(g)` is a two-sided inverse of `F(f)`:`F(g) ∘ F(f) = F(g ∘ f) = F(id) = id`, and the same the other way round. Only the two functorlaws are used. -/theorem map_inverse {C : Type u} [Category.{v} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D) {X Y : C} {f : X ⟶ Y} {g : Y ⟶ X} (h₁ : f ≫ g = 𝟙 X) (h₂ : g ≫ f = 𝟙 Y) : F.map f ≫ F.map g = 𝟙 (F.obj X) ∧ F.map g ≫ F.map f = 𝟙 (F.obj Y) := by constructor · rw [← F.map_comp, h₁, F.map_id] · rw [← F.map_comp, h₂, F.map_id]
iso_of_isotheoremProved here from basic factsNo axioms
iso_of_isoLean 4Proved here from basic factsFormally verified
/-- **Functors preserve isomorphic objects.** An isomorphism `e : X ≅ Y` in `C` gives anisomorphism `F(X) ≅ F(Y)` in `D`, built from `map_inverse`. Read backwards this is theimpossibility tool of the lesson: if `F(X)` and `F(Y)` are *not* isomorphic, neither are `X`and `Y`. (Mathlib's name for this construction is `Functor.mapIso`.) -/theorem iso_of_iso {C : Type u} [Category.{v} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D) {X Y : C} (e : X ≅ Y) : Nonempty (F.obj X ≅ F.obj Y) := ⟨⟨F.map e.hom, F.map e.inv, (map_inverse F e.hom_inv_id e.inv_hom_id).1, (map_inverse F e.hom_inv_id e.inv_hom_id).2⟩⟩
map_isIso_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
map_isIso_libraryLean 4Applies a library theoremFormally verified
/-- Mathlib's version: if `f` is an isomorphism then so is `F.map f`. This applies the instance`CategoryTheory.Functor.map_isIso`. -/theorem map_isIso_library {C : Type u} [Category.{v} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [IsIso f] : IsIso (F.map f) := Functor.map_isIso F f
zmod4_not_iso_kleintheoremProved here from basic factspropext, Classical.choice, Quot.sound
zmod4_not_iso_kleinLean 4Proved here from basic factsFormally verified
/-- **`ℤ/4` and `ℤ/2 × ℤ/2` are not isomorphic groups.** The lesson's argument applies thefunctor `G ↦ 2G = {x + x}` (or, dually, `Hom(ℤ/2, −)`): it sends `ℤ/4` to a group with twoelements and `ℤ/2 × ℤ/2` to the trivial group. Unwound to elements: in `ℤ/2 × ℤ/2` every`y` has `y + y = 0`, so an additive isomorphism `e` would give `e(2) = e(1) + e(1) = 0 = e(0)`,and injectivity would force `2 = 0` in `ℤ/4`, which is false. -/theorem zmod4_not_iso_klein : IsEmpty (ZMod 4 ≃+ ZMod 2 × ZMod 2) := by constructor intro e have hdouble : ∀ y : ZMod 2 × ZMod 2, y + y = 0 := by decide have h2 : e 2 = e 0 := by calc e 2 = e (1 + 1) := rfl _ = e 1 + e 1 := map_add e 1 1 _ = 0 := hdouble (e 1) _ = e 0 := (map_zero e).symm have : (2 : ZMod 4) = 0 := e.injective h2 exact absurd this (by decide)
/-- **The covariant power-set functor** `P : Set → Set`. It sends a set `X` to the set of itssubsets, and a function `f : X → Y` to the direct-image map `S ↦ f(S)`.The functor laws are `id(S) = S` (`Set.image_id`) and `(g ∘ f)(S) = g(f(S))` (`Set.image_comp`). -/def powerset : Type u ⥤ Type u where obj X := Set X map f := ↾(fun S => (fun x => f x) '' S) map_id X := by ext S simp map_comp f g := by ext S simp [Set.image_image]
/-- **The contravariant power-set functor** `P* : Setᵒᵖ → Set`. It sends a function`f : X → Y` to the preimage map `T ↦ f⁻¹(T)`, which goes the *other way*, from subsets of `Y`to subsets of `X`. So it is a functor out of the opposite category: the laws are`id⁻¹(T) = T` and `(g ∘ f)⁻¹(T) = f⁻¹(g⁻¹(T))` — note the reversed order. -/def powersetContra : (Type u)ᵒᵖ ⥤ Type u where obj X := Set X.unop map f := ↾(fun T => (fun x => f.unop x) ⁻¹' T) map_id X := by ext T simp map_comp f g := by ext T simp [Set.preimage_preimage]
/-- **The list functor.** It sends a set `X` to the set `List X` of finite words in `X`, and afunction `f` to "apply `f` letter by letter" (`List.map f`). The laws are `List.map_id` and`List.map_map`. `List X` with concatenation is the free monoid on `X` (see `list_map_append`and the lesson on universal properties). -/def listFunctor : Type u ⥤ Type u where obj X := List X map f := ↾(List.map (fun x => f x)) map_id X := by ext l simp map_comp f g := by ext l simp [List.map_map, Function.comp_def]
list_map_appendtheoremApplies a library theorempropext
list_map_appendLean 4Applies a library theoremFormally verified
/-- `List.map f` is a **monoid homomorphism** for concatenation: it preserves the empty wordand `map f (l ++ m) = map f l ++ map f m`. So the list functor really lands in monoids. Thisapplies `List.map_nil` and `List.map_append`. -/theorem list_map_append {X Y : Type u} (f : X → Y) (l m : List X) : List.map f [] = [] ∧ List.map f (l ++ m) = List.map f l ++ List.map f m := ⟨List.map_nil, List.map_append⟩
free_monoid_librarytheoremApplies a library theorempropext, Quot.sound
free_monoid_libraryLean 4Applies a library theoremFormally verified
/-- Mathlib's **free monoid functor** `MonCat.free : Type u ⥤ MonCat` sends a set `X` to the freemonoid `FreeMonoid X` (lists with concatenation) and a function to the homomorphism that renamesletters: a one-letter word `[a]` goes to `[f a]`. This applies `MonCat.free` and`FreeMonoid.map_of`. -/theorem free_monoid_library {X Y : Type u} (f : X ⟶ Y) (a : X) : (MonCat.free.map f).hom (FreeMonoid.of a) = FreeMonoid.of (f a) := FreeMonoid.map_of _ a
/-- **The hom functor** `Hom(A, −) : C → Set`. It sends an object `B` to the set of morphisms`A ⟶ B`, and a morphism `f : B ⟶ B'` to "compose with `f`": `g ↦ f ∘ g` (`g ≫ f` in Mathlib).The functor laws are exactly the axioms of a category: `id ∘ g = g` (`Category.comp_id`) and`(f' ∘ f) ∘ g = f' ∘ (f ∘ g)` (`Category.assoc`). Mathlib calls it `coyoneda.obj (op A)`. -/def homFunctor {C : Type u} [Category.{v} C] (A : C) : C ⥤ Type v where obj B := A ⟶ B map f := ↾(fun g => g ≫ f) map_id B := by ext g simp map_comp f f' := by ext g simp
/-- **The contravariant hom functor** `Hom(−, A) : Cᵒᵖ → Set`, sending `f : B' ⟶ B` to"precompose with `f`": `g ↦ g ∘ f`. Precomposition reverses the direction of arrows, so this isa functor out of `Cᵒᵖ`. Mathlib calls it `yoneda.obj A`. -/def homFunctorContra {C : Type u} [Category.{v} C] (A : C) : Cᵒᵖ ⥤ Type v where obj B := B.unop ⟶ A map f := ↾(fun g => f.unop ≫ g) map_id B := by ext g simp map_comp f f' := by ext g simp
comp_assoc_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
comp_assoc_libraryLean 4Applies a library theoremFormally verified
/-- **Functors compose, associatively.** `F ⋙ G` is "first `F`, then `G`", and composition offunctors is associative (on the nose). Together with identity functors this makes smallcategories and functors into a category, Mathlib's `Cat`. This applies `Functor.assoc`. -/theorem comp_assoc_library {A : Type u} [Category.{v} A] {B : Type u₂} [Category.{v₂} B] {C : Type w} [Category.{w} C] {D : Type u} [Category.{v} D] (F : A ⥤ B) (G : B ⥤ C) (H : C ⥤ D) : (F ⋙ G) ⋙ H = F ⋙ (G ⋙ H) := Functor.assoc F G H
map_injective_of_retractiontheoremProved here from basic factspropext, Quot.sound
map_injective_of_retractionLean 4Proved here from basic factsFormally verified
/-- **Functors preserve retractions.** If `r ∘ i = id_S` (here `i ≫ r = 𝟙 S`), then`F(r) ∘ F(i) = id_{F(S)}` for every functor `F`; for a functor to sets this makes `F(i)`injective, since `F(i)(a) = F(i)(b)` gives `a = F(r)(F(i)(a)) = F(r)(F(i)(b)) = b`. -/theorem map_injective_of_retraction {C : Type u} [Category.{v} C] (F : C ⥤ Type w) {S D : C} (i : S ⟶ D) (r : D ⟶ S) (h : i ≫ r = 𝟙 S) : Function.Injective (F.map i) := by have hFr : F.map i ≫ F.map r = 𝟙 (F.obj S) := by rw [← F.map_comp, h, F.map_id] intro a b hab calc a = (F.map i ≫ F.map r) a := by rw [hFr]; rfl _ = F.map r (F.map i a) := rfl _ = F.map r (F.map i b) := by rw [hab] _ = (F.map i ≫ F.map r) b := rfl _ = b := by rw [hFr]; rfl
no_retractiontheoremProved here from basic factspropext, Quot.sound
no_retractionLean 4Proved here from basic factsFormally verified
/-- **The shape of the no-retraction theorem.** Suppose a functor `F` to sets sends `D` to a setwith at most one element and `S` to a set with two different elements. Then there is **no**retraction `r : D → S` of any `i : S → D` (no `r` with `r ∘ i = id_S`): `F(i)` would be aninjective map from a set with two elements into a set with one.For the circle `S¹` inside the disc `D²` and `F = π₁` (fundamental group, a functor from pointedspaces to groups, then to sets): `π₁(D²)` is trivial and `π₁(S¹) ≅ ℤ` is not, so the disc does notretract onto its boundary circle. -/theorem no_retraction {C : Type u} [Category.{v} C] (F : C ⥤ Type w) {S D : C} (i : S ⟶ D) [Subsingleton (F.obj D)] {a b : F.obj S} (hab : a ≠ b) : ¬ ∃ r : D ⟶ S, i ≫ r = 𝟙 S := by rintro ⟨r, h⟩ exact hab (map_injective_of_retraction F i r h (Subsingleton.elim _ _))
not_reflects_isotheoremProved here from basic factspropext, Classical.choice, Quot.sound
not_reflects_isoLean 4Proved here from basic factsFormally verified
/-- **A functor can send a non-isomorphism to an isomorphism.** In the poset `0 < 1` (Lean's`Fin 2`) regarded as a category, the morphism `0 ⟶ 1` is not an isomorphism (an inverse would bea morphism `1 ⟶ 0`, that is `1 ≤ 0`). But the constant functor to a one-element set sends it tothe identity map, which is an isomorphism. So `F(f)` invertible does not force `f` invertible. -/theorem not_reflects_iso : ∃ (F : Fin 2 ⥤ Type) (f : (0 : Fin 2) ⟶ 1), IsIso (F.map f) ∧ ¬ IsIso f := by have h01 : (0 : Fin 2) ≤ 1 := by decide refine ⟨(Functor.const (Fin 2)).obj PUnit, homOfLE h01, ?_, ?_⟩ · -- the constant functor sends every morphism to an identity show IsIso (𝟙 PUnit) infer_instance · intro hf have h10 : (1 : Fin 2) ≤ 0 := leOfHom (inv (homOfLE h01)) exact absurd h10 (by decide)
/-- Functors carry inverse pairs to inverse pairs. Hint: rewrite with `← F.map_comp`, then usethe hypothesis and `F.map_id`. -/theorem map_inverse {C : Type u} [Category.{v} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D) {X Y : C} {f : X ⟶ Y} {g : Y ⟶ X} (h₁ : f ≫ g = 𝟙 X) (h₂ : g ≫ f = 𝟙 Y) : F.map f ≫ F.map g = 𝟙 (F.obj X) ∧ F.map g ≫ F.map f = 𝟙 (F.obj Y) := by sorry
Show the compiled solution
map_inverseLean 4Proved here from basic factsFormally verified
/-- **Functors carry inverse pairs to inverse pairs.** If `g` is a two-sided inverse of `f`,then `F(g)` is a two-sided inverse of `F(f)`:`F(g) ∘ F(f) = F(g ∘ f) = F(id) = id`, and the same the other way round. Only the two functorlaws are used. -/theorem map_inverse {C : Type u} [Category.{v} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D) {X Y : C} {f : X ⟶ Y} {g : Y ⟶ X} (h₁ : f ≫ g = 𝟙 X) (h₂ : g ≫ f = 𝟙 Y) : F.map f ≫ F.map g = 𝟙 (F.obj X) ∧ F.map g ≫ F.map f = 𝟙 (F.obj Y) := by constructor · rw [← F.map_comp, h₁, F.map_id] · rw [← F.map_comp, h₂, F.map_id]
/-- `ℤ/4` and `ℤ/2 × ℤ/2` are not isomorphic. Hint: every `y : ZMod 2 × ZMod 2` has`y + y = 0` (`by decide`), so `e 2 = e 1 + e 1 = 0 = e 0`; then use `e.injective`. -/theorem zmod4_not_iso_klein : IsEmpty (ZMod 4 ≃+ ZMod 2 × ZMod 2) := by sorry
Show the compiled solution
zmod4_not_iso_kleinLean 4Proved here from basic factsFormally verified
/-- **`ℤ/4` and `ℤ/2 × ℤ/2` are not isomorphic groups.** The lesson's argument applies thefunctor `G ↦ 2G = {x + x}` (or, dually, `Hom(ℤ/2, −)`): it sends `ℤ/4` to a group with twoelements and `ℤ/2 × ℤ/2` to the trivial group. Unwound to elements: in `ℤ/2 × ℤ/2` every`y` has `y + y = 0`, so an additive isomorphism `e` would give `e(2) = e(1) + e(1) = 0 = e(0)`,and injectivity would force `2 = 0` in `ℤ/4`, which is false. -/theorem zmod4_not_iso_klein : IsEmpty (ZMod 4 ≃+ ZMod 2 × ZMod 2) := by constructor intro e have hdouble : ∀ y : ZMod 2 × ZMod 2, y + y = 0 := by decide have h2 : e 2 = e 0 := by calc e 2 = e (1 + 1) := rfl _ = e 1 + e 1 := map_add e 1 1 _ = 0 := hdouble (e 1) _ = e 0 := (map_zero e).symm have : (2 : ZMod 4) = 0 := e.injective h2 exact absurd this (by decide)