/-- **Currying.** Functions of two arguments `A × B → C` correspond bijectively to functions`A → (B → C)` returning functions: `h ↦ (a ↦ (b ↦ h (a, b)))`, with inverse "uncurrying". This isthe hom-set bijection `Hom(A × B, C) ≅ Hom(A, C^B)` of the adjunction `− × B ⊣ (−)^B`.(Mathlib: `Equiv.curry`.) -/def curryEquiv (A B C : Type u) : (A × B → C) ≃ (A → B → C) where toFun h a b := h (a, b) invFun k p := k p.1 p.2 left_inv _ := rfl right_inv _ := rfl
curry_naturaltheoremProved here from basic factsQuot.sound
curry_naturalLean 4Proved here from basic factsFormally verified
/-- **The currying bijection is natural in `A` and in `C`.** Precomposing with `u : A' → A` (on`A × B`, with `u × id`) and postcomposing with `v : C → C'` before currying gives the same ascurrying first and then precomposing with `u` and postcomposing with `v` pointwise. Both sides are`a' ↦ b ↦ v (h (u a', b))`, so Lean accepts `rfl`. -/theorem curry_natural (u : A' → A) (v : C → C') (h : A × B → C) : curryEquiv A' B C' (v ∘ h ∘ Prod.map u id) = fun a' => v ∘ curryEquiv A B C h (u a') := rfl
/-- The **unit** of the currying adjunction, `η_A : A → (B → A × B)`, `a ↦ (b ↦ (a, b))`: thecurried form of the identity of `A × B`. -/def curryUnit (A B : Type u) : A → B → A × B := fun a b => (a, b)
/-- The **counit** of the currying adjunction, `ε_C : (B → C) × B → C`, evaluation`(φ, b) ↦ φ b`: the uncurried form of the identity of `B → C`. -/def curryCounit (B C : Type u) : (B → C) × B → C := fun p => p.1 p.2
curry_trianglestheoremProved here from basic factsNo axioms
curry_trianglesLean 4Proved here from basic factsFormally verified
/-- **The triangle identities for currying.**1. `ε_{A × B} ∘ (η_A × id_B) = id`: pair `(a, b)` ↦ `(η a, b)` ↦ `η a b = (a, b)`.2. `(ε_C)^B ∘ η_{C^B} = id`: `φ` ↦ `(b ↦ (φ, b))` ↦ `(b ↦ φ b) = φ`.Both hold by computation. -/theorem curry_triangles : (curryCounit B (A × B) ∘ Prod.map (curryUnit A B) id = id) ∧ ((fun (k : B → (B → C) × B) => curryCounit B C ∘ k) ∘ curryUnit (B → C) B = id) := ⟨rfl, rfl⟩
free_monoid_lifttheoremApplies a library theorempropext, Quot.sound
free_monoid_liftLean 4Applies a library theoremFormally verified
/-- **Free monoid ⊣ forgetful.** Functions `α → M` into (the underlying set of) a monoidcorrespond bijectively to monoid homomorphisms `FreeMonoid α →* M`, by extending a function towords multiplicatively: `Hom_Mon(F α, M) ≅ Hom_Set(α, U M)`. This is Mathlib's `FreeMonoid.lift`,and naturality in `M` is `FreeMonoid.comp_lift`. -/theorem free_monoid_lift {N : Type u} [Monoid N] (g : M →* N) (f : α → M) : Function.Bijective (FreeMonoid.lift : (α → M) → (FreeMonoid α →* M)) ∧ g.comp (FreeMonoid.lift f) = FreeMonoid.lift (g ∘ f) := ⟨FreeMonoid.lift.bijective, FreeMonoid.comp_lift g f⟩
free_hom_exttheoremProved here from basic factspropext, Quot.sound
free_hom_extLean 4Proved here from basic factsFormally verified
/-- **Uniqueness in the universal property of the free monoid.** Two homomorphisms out of`FreeMonoid α` that agree on the generators `of x` agree everywhere: by induction on words, using`f 1 = 1 = g 1` and `f (of x * w) = f (of x) * f w`. -/theorem free_hom_ext {f g : FreeMonoid α →* M} (h : ∀ x, f (FreeMonoid.of x) = g (FreeMonoid.of x)) : f = g := by refine DFunLike.ext _ _ fun w => ?_ induction w using FreeMonoid.inductionOn' with | one => rw [map_one, map_one] | of_mul x w ih => rw [map_mul, map_mul, h x, ih]
unit_not_surjectivetheoremProved here from basic factspropext, Quot.sound
unit_not_surjectiveLean 4Proved here from basic factsFormally verified
/-- **The unit of an adjunction need not be an isomorphism.** The unit of free ⊣ forgetful at aset `α` is `of : α → FreeMonoid α`. It is never surjective: the empty word `1` is not a generator.So this adjunction is not an equivalence. -/theorem unit_not_surjective : ¬ Function.Surjective (FreeMonoid.of : α → FreeMonoid α) := by intro hs obtain ⟨x, hx⟩ := hs 1 exact FreeMonoid.of_ne_one x hx
image_preimagetheoremApplies a library theorempropext, Classical.choice, Quot.sound
image_preimageLean 4Applies a library theoremFormally verified
/-- **Image ⊣ preimage.** For `f : α → β`, `f '' S ⊆ T ↔ S ⊆ f ⁻¹' T`: direct image is left adjointto inverse image between the power-set lattices. This is Mathlib's `Set.image_preimage`. -/theorem image_preimage {α β : Type u} (f : α → β) : GaloisConnection (Set.image f) (Set.preimage f) := Set.image_preimage
left_adjoint_suptheoremProved here from basic factspropext, Quot.sound
left_adjoint_supLean 4Proved here from basic factsFormally verified
/-- **Left adjoints preserve joins** (binary coproducts in a poset). If `l ⊣ u`, then`l (a ⊔ b) = l a ⊔ l b`. (≤): `a ≤ u (l a ⊔ l b)` because `l a ≤ l a ⊔ l b`, likewise for `b`,so `a ⊔ b ≤ u (l a ⊔ l b)`, i.e. `l (a ⊔ b) ≤ l a ⊔ l b`. (≥): `l` is monotone.(Mathlib: `GaloisConnection.l_sup`.) -/theorem left_adjoint_sup [SemilatticeSup α] [SemilatticeSup β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (a b : α) : l (a ⊔ b) = l a ⊔ l b := by apply le_antisymm · rw [gc] exact sup_le ((gc _ _).1 le_sup_left) ((gc _ _).1 le_sup_right) · exact sup_le (gc.monotone_l le_sup_left) (gc.monotone_l le_sup_right)
right_adjoint_uniquetheoremProved here from basic factsQuot.sound
right_adjoint_uniqueLean 4Proved here from basic factsFormally verified
/-- **Right adjoints are unique.** If `l ⊣ u` and `l ⊣ u'` between partial orders, then `u = u'`:for every `b` and every `a`, `a ≤ u b ↔ l a ≤ b ↔ a ≤ u' b`, and an element is determined by itslower set. (This is the poset case of uniqueness of adjoints up to unique isomorphism.) -/theorem right_adjoint_unique [PartialOrder α] [Preorder β] {l : α → β} {u u' : β → α} (gc : GaloisConnection l u) (gc' : GaloisConnection l u') : u = u' := by funext b apply le_antisymm · exact (gc' _ _).1 ((gc _ _).2 le_rfl) · exact (gc _ _).1 ((gc' _ _).2 le_rfl)
const_true_no_right_adjointtheoremProved here from basic factspropext, Classical.choice, Quot.sound
const_true_no_right_adjointLean 4Proved here from basic factsFormally verified
/-- **Using preservation to rule out an adjoint.** The constant map `Bool → Bool` with value`true` is monotone, but it sends `⊥ = false` to `true ≠ ⊥`. Left adjoints preserve `⊥`(`left_adjoint_bot`), so it has no right adjoint. -/theorem const_true_no_right_adjoint : ¬ ∃ u : Bool → Bool, GaloisConnection (fun _ => true) u := by rintro ⟨u, gc⟩ have h : true = false := left_adjoint_bot gc exact Bool.noConfusion h
adjoint_functor_theorem_latticestheoremProved here from basic factspropext, Classical.choice, Quot.sound
adjoint_functor_theorem_latticesLean 4Proved here from basic factsFormally verified
/-- **The adjoint functor theorem for complete lattices.** If `u : β → α` between completelattices preserves all infima (all limits of the poset), then `u` has a left adjoint, given bythe formula `l a = ⨅ { b | a ≤ u b }` (the "best approximation from above").Proof: `u` is monotone (if `b ≤ b'` then `u b = u (⨅ {b, b'}) = u b ⊓ u b' ≤ u b'`). If`a ≤ u b` then `b` belongs to the set, so `l a ≤ b`. Conversely `u (l a)` is the infimum ofthe `u b` with `a ≤ u b`, all of which are `≥ a`; so `a ≤ u (l a) ≤ u b` whenever `l a ≤ b`. -/theorem adjoint_functor_theorem_lattices [CompleteLattice α] [CompleteLattice β] (u : β → α) (hu : ∀ S : Set β, u (sInf S) = sInf (u '' S)) : GaloisConnection (fun a => sInf {b | a ≤ u b}) u := by have mono : Monotone u := by intro b b' h have hpair : u (sInf {b, b'}) = sInf (u '' {b, b'}) := hu {b, b'} rw [sInf_pair, inf_eq_left.mpr h, Set.image_pair, sInf_pair] at hpair rw [hpair] exact inf_le_right intro a b constructor · intro h refine le_trans ?_ (mono h) rw [hu] exact le_sInf (by rintro _ ⟨c, hc, rfl⟩; exact hc) · intro h exact sInf_le h
left_adjoint_uniquetheoremApplies a library theorempropext, Classical.choice, Quot.sound
left_adjoint_uniqueLean 4Applies a library theoremFormally verified
/-- **Left adjoints are unique up to natural isomorphism**: if `F ⊣ G` and `F' ⊣ G` then`F ≅ F'`. This applies Mathlib's `Adjunction.leftAdjointUniq` (the isomorphism is moreoverunique compatible with the units). -/theorem left_adjoint_unique {F F' : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) (adj' : F' ⊣ G) : Nonempty (F ≅ F') := ⟨Adjunction.leftAdjointUniq adj adj'⟩
right_adjoint_preserves_limitstheoremApplies a library theorempropext, Classical.choice, Quot.sound
right_adjoint_preserves_limitsLean 4Applies a library theoremFormally verified
/-- **Right adjoints preserve limits, left adjoints preserve colimits** (RAPL). This appliesMathlib's `Adjunction.rightAdjoint_preservesLimits` and `Adjunction.leftAdjoint_preservesColimits`;the lesson proves it from the hom-set bijection. -/theorem right_adjoint_preserves_limits {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : PreservesLimitsOfSize.{v₂, u₂} G ∧ PreservesColimitsOfSize.{v₁, u₁} F := ⟨adj.rightAdjoint_preservesLimits, adj.leftAdjoint_preservesColimits⟩
/-- **Every adjunction induces a monad** `G ∘ F` on `C`, with unit `η` and multiplication`G ε F : GFGF ⇒ GF`. This is Mathlib's `Adjunction.toMonad`; see the lesson on monads. -/def adjunctionMonad {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : Monad C := adj.toMonad
freyd_adjoint_functor_theoremtheoremApplies a library theorempropext, Classical.choice, Quot.sound
freyd_adjoint_functor_theoremLean 4Applies a library theoremFormally verified
/-- **Freyd's general adjoint functor theorem.** If `D` is complete (and locally small) and`G : D ⥤ C` preserves limits and satisfies the *solution set condition* — for each object `A` of`C`, a set of arrows `A ⟶ G Bᵢ` through which every arrow `A ⟶ G X` factors — then `G` has aleft adjoint. This applies Mathlib's `isRightAdjoint_of_preservesLimits_of_solutionSetCondition`;`adjoint_functor_theorem_lattices` is the special case of complete lattices, where the solutionset can be taken to be everything. -/theorem freyd_adjoint_functor_theorem {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₁} D] [HasLimits D] (G : D ⥤ C) [PreservesLimits G] (hG : SolutionSetCondition.{v₁} G) : G.IsRightAdjoint := isRightAdjoint_of_preservesLimits_of_solutionSetCondition G hG
/-- **Tensor–hom adjunction** `− ⊗ N ⊣ Hom(N, −)` for modules over a commutative ring:bilinear maps `M → N → P` (that is, linear maps `M → Hom(N, P)`) correspond to linear maps`M ⊗ N → P`. This is Mathlib's `TensorProduct.lift.equiv`, the linear analogue of currying. -/noncomputable def tensorHom (R M N P : Type u) [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] : (M →ₗ[R] N →ₗ[R] P) ≃ₗ[R] (TensorProduct R M N →ₗ[R] P) := TensorProduct.lift.equiv (RingHom.id R) M N P
option_no_left_adjointtheoremProved here from basic factspropext, Classical.choice, Quot.sound
option_no_left_adjointLean 4Proved here from basic factsFormally verified
/-- **"Adjoin a point" has no left adjoint on types.** Let `G X = Option X` (that is, `X ⊔ {∗}`).If `F ⊣ G`, then `G` preserves limits (Mathlib's `rightAdjoint_preservesLimits`), in particular theterminal object, so `Option PUnit` would be terminal. But there are two different maps`PUnit → Option PUnit` (constant `none`, constant `some ()`), and a terminal object admits onlyone map from each object. -/theorem option_no_left_adjoint : ¬ ∃ F : Type u ⥤ Type u, Nonempty (F ⊣ ofTypeFunctor Option) := by rintro ⟨F, ⟨adj⟩⟩ have := adj.rightAdjoint_preservesLimits have hT : IsTerminal ((ofTypeFunctor Option).obj PUnit) := IsTerminal.isTerminalObj _ _ Types.isTerminalPUnit have h := hT.hom_ext (↾fun _ : PUnit => (none : Option PUnit)) (↾fun _ : PUnit => (some PUnit.unit : Option PUnit)) have h' := ConcreteCategory.congr_hom h PUnit.unit simp at h'
option_no_right_adjointtheoremProved here from basic factspropext, Classical.choice, Quot.sound
option_no_right_adjointLean 4Proved here from basic factsFormally verified
/-- **…and no right adjoint either.** A left adjoint preserves colimits, in particular the initialobject `PEmpty`. But `Option PEmpty` has an element (`none`), so there are two different maps fromit to a two-element type, and it is not initial. (Changing the target category repairs this:`X ↦ X ⊔ {∗}` is left adjoint to the forgetful functor from *pointed* sets to sets.) -/theorem option_no_right_adjoint : ¬ ∃ G : Type u ⥤ Type u, Nonempty (ofTypeFunctor Option ⊣ G) := by rintro ⟨G, ⟨adj⟩⟩ have := adj.leftAdjoint_preservesColimits have hI : IsInitial ((ofTypeFunctor Option).obj PEmpty) := IsInitial.isInitialObj _ _ Types.isInitialPEmpty have h := hI.hom_ext (↾fun _ : Option PEmpty => (ULift.up true : ULift.{u} Bool)) (↾fun _ : Option PEmpty => (ULift.up false : ULift.{u} Bool)) have h' := ConcreteCategory.congr_hom h (none : Option PEmpty.{u + 1}) exact Bool.noConfusion (congrArg ULift.down h' : true = false)
/-- Right adjoints between posets are unique.Hint: `funext b`, then `le_antisymm`. For `u b ≤ u' b`, use `gc' (u b) b` to reduce to`l (u b) ≤ b`, which is `(gc (u b) b).2 le_rfl`. The other inequality is symmetric. -/theorem right_adjoint_unique [PartialOrder α] [Preorder β] {l : α → β} {u u' : β → α} (gc : GaloisConnection l u) (gc' : GaloisConnection l u') : u = u' := by sorry
Show the compiled solution
right_adjoint_uniqueLean 4Proved here from basic factsFormally verified
/-- **Right adjoints are unique.** If `l ⊣ u` and `l ⊣ u'` between partial orders, then `u = u'`:for every `b` and every `a`, `a ≤ u b ↔ l a ≤ b ↔ a ≤ u' b`, and an element is determined by itslower set. (This is the poset case of uniqueness of adjoints up to unique isomorphism.) -/theorem right_adjoint_unique [PartialOrder α] [Preorder β] {l : α → β} {u u' : β → α} (gc : GaloisConnection l u) (gc' : GaloisConnection l u') : u = u' := by funext b apply le_antisymm · exact (gc' _ _).1 ((gc _ _).2 le_rfl) · exact (gc _ _).1 ((gc' _ _).2 le_rfl)
/-- Left adjoints preserve binary joins.Hint: `le_antisymm`. For `l (a ⊔ b) ≤ l a ⊔ l b`, rewrite with `gc` to get`a ⊔ b ≤ u (l a ⊔ l b)` and use `sup_le`, turning each `l a ≤ l a ⊔ l b` back with `gc`.For the other inequality use `gc.monotone_l`. -/theorem left_adjoint_sup [SemilatticeSup α] [SemilatticeSup β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (a b : α) : l (a ⊔ b) = l a ⊔ l b := by sorry
Show the compiled solution
left_adjoint_supLean 4Proved here from basic factsFormally verified
/-- **Left adjoints preserve joins** (binary coproducts in a poset). If `l ⊣ u`, then`l (a ⊔ b) = l a ⊔ l b`. (≤): `a ≤ u (l a ⊔ l b)` because `l a ≤ l a ⊔ l b`, likewise for `b`,so `a ⊔ b ≤ u (l a ⊔ l b)`, i.e. `l (a ⊔ b) ≤ l a ⊔ l b`. (≥): `l` is monotone.(Mathlib: `GaloisConnection.l_sup`.) -/theorem left_adjoint_sup [SemilatticeSup α] [SemilatticeSup β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (a b : α) : l (a ⊔ b) = l a ⊔ l b := by apply le_antisymm · rw [gc] exact sup_le ((gc _ _).1 le_sup_left) ((gc _ _).1 le_sup_right) · exact sup_le (gc.monotone_l le_sup_left) (gc.monotone_l le_sup_right)