/-- The Yoneda map: a natural transformation `α : Hom(A, −) ⇒ F` goes to the element`α_A(id_A) ∈ F(A)` — "where `α` sends the identity". -/def toElement {A : C} {F : C ⥤ Type v} (α : coyoneda.obj (op A) ⟶ F) : F.obj A := α.app A (𝟙 A)
/-- The inverse map: an element `x ∈ F(A)` gives the natural transformation`Hom(A, −) ⇒ F` whose component at `B` sends `f : A ⟶ B` to `F(f)(x)`. Naturality isfunctoriality of `F`: `F(f ≫ g)(x) = F(g)(F(f)(x))`. -/def ofElement {A : C} {F : C ⥤ Type v} (x : F.obj A) : coyoneda.obj (op A) ⟶ F where app B := ↾fun f => F.map f x naturality B B' g := by ext f exact Functor.map_comp_apply F f g x
ofElement_toElementtheoremProved here from basic factspropext, Classical.choice, Quot.sound
ofElement_toElementLean 4Proved here from basic factsFormally verified
/-- **The heart of the Yoneda lemma**: a natural transformation `α : Hom(A, −) ⇒ F` isdetermined by `α_A(id_A)`. For `f : A ⟶ B`, naturality of `α` along `f` applied to `id_A` gives`α_B(f) = α_B(id_A ≫ f) = F(f)(α_A(id_A))`. -/theorem ofElement_toElement {A : C} {F : C ⥤ Type v} (α : coyoneda.obj (op A) ⟶ F) : ofElement (toElement α) = α := by ext B f calc F.map f (α.app A (𝟙 A)) = α.app B ((coyoneda.obj (op A)).map f (𝟙 A)) := (NatTrans.naturality_apply α f _).symm _ = α.app B (𝟙 A ≫ f) := rfl _ = α.app B f := by rw [Category.id_comp]
toElement_ofElementtheoremProved here from basic factspropext, Classical.choice, Quot.sound
toElement_ofElementLean 4Proved here from basic factsFormally verified
/-- The other composite: the transformation built from `x` sends `id_A` to `F(id_A)(x) = x`. -/theorem toElement_ofElement {A : C} {F : C ⥤ Type v} (x : F.obj A) : toElement (ofElement x) = x := Functor.map_id_apply F A x
toElement_natural_functortheoremProved here from basic factspropext, Classical.choice, Quot.sound
toElement_natural_functorLean 4Proved here from basic factsFormally verified
/-- The Yoneda bijection is **natural in `F`**: following `α` by a transformation`β : F ⇒ G` corresponds to applying `β_A` to the element. -/theorem toElement_natural_functor {A : C} {F G : C ⥤ Type v} (α : coyoneda.obj (op A) ⟶ F) (β : F ⟶ G) : toElement (α ≫ β) = β.app A (toElement α) := rfl
toElement_natural_objecttheoremProved here from basic factspropext, Classical.choice, Quot.sound
toElement_natural_objectLean 4Proved here from basic factsFormally verified
/-- The Yoneda bijection is **natural in `A`**: for `f : A ⟶ A'`, precomposing `α` with`Hom(f, −) : Hom(A', −) ⇒ Hom(A, −)` corresponds to applying `F(f)` to the element. -/theorem toElement_natural_object {A A' : C} {F : C ⥤ Type v} (f : A ⟶ A') (α : coyoneda.obj (op A) ⟶ F) : toElement (coyoneda.map f.op ≫ α) = F.map f (toElement α) := by calc toElement (coyoneda.map f.op ≫ α) = α.app A' (f ≫ 𝟙 A') := rfl _ = α.app A' f := by rw [Category.comp_id] _ = (ofElement (toElement α)).app A' f := by rw [ofElement_toElement] _ = F.map f (toElement α) := rfl
nat_trans_representablestheoremProved here from basic factspropext, Classical.choice, Quot.sound
nat_trans_representablesLean 4Proved here from basic factsFormally verified
/-- **Full and faithful**: every natural transformation `α : Hom(A, −) ⇒ Hom(B, −)` isprecomposition with exactly one arrow `g : B ⟶ A`, namely `g = α_A(id_A)`. This is the Yonedalemma for `F = Hom(B, −)`; it says that `coyoneda` is full and faithful. -/theorem nat_trans_representables {A B : C} (α : coyoneda.obj (op A) ⟶ coyoneda.obj (op B)) : ∃! g : B ⟶ A, coyoneda.map g.op = α := by refine ⟨toElement α, ?_, ?_⟩ · calc coyoneda.map (toElement α).op = ofElement (toElement α) := by ext X f rfl _ = α := ofElement_toElement α · intro g hg rw [← hg] exact (Category.comp_id g).symm
iso_of_corepresentable_isotheoremProved here from basic factspropext, Classical.choice, Quot.sound
iso_of_corepresentable_isoLean 4Proved here from basic factsFormally verified
/-- **An object is determined by the arrows out of it.** If `Hom(A, −) ≅ Hom(B, −)` naturally,then `A ≅ B`. With `g = e(id_A) : B ⟶ A` and `h = e⁻¹(id_B) : A ⟶ B`, the components of `e` and`e⁻¹` are precomposition with `g` and `h`, and `e⁻¹ ∘ e = id` evaluated at `id_A` reads`h ≫ g = id_A`; similarly `g ≫ h = id_B`. -/theorem iso_of_corepresentable_iso {A B : C} (e : coyoneda.obj (op A) ≅ coyoneda.obj (op B)) : Nonempty (A ≅ B) := by have hom_app : ∀ (X : C) (f : A ⟶ X), e.hom.app X f = toElement e.hom ≫ f := fun X f => calc e.hom.app X f = (ofElement (toElement e.hom)).app X f := by rw [ofElement_toElement] _ = toElement e.hom ≫ f := rfl have inv_app : ∀ (X : C) (f : B ⟶ X), e.inv.app X f = toElement e.inv ≫ f := fun X f => calc e.inv.app X f = (ofElement (toElement e.inv)).app X f := by rw [ofElement_toElement] _ = toElement e.inv ≫ f := rfl refine ⟨⟨toElement e.inv, toElement e.hom, ?_, ?_⟩⟩ · calc toElement e.inv ≫ toElement e.hom = e.inv.app A (toElement e.hom) := (inv_app A _).symm _ = e.inv.app A (e.hom.app A (𝟙 A)) := rfl _ = 𝟙 A := by simp · calc toElement e.hom ≫ toElement e.inv = e.hom.app B (toElement e.inv) := (hom_app B _).symm _ = e.hom.app B (e.inv.app B (𝟙 B)) := rfl _ = 𝟙 B := by simp
yoneda_lemma_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
yoneda_lemma_libraryLean 4Applies a library theoremFormally verified
/-- **The Yoneda lemma, contravariant form, from Mathlib**: for a presheaf `P : Cᵒᵖ ⥤ Type`,`α ↦ α_A(id_A)` is a bijection `Nat(Hom(−, A), P) ≃ P(A)`. This applies Mathlib's`yonedaEquiv`. -/theorem yoneda_lemma_library (P : Cᵒᵖ ⥤ Type v) (A : C) : Function.Bijective (fun α : yoneda.obj A ⟶ P => α.app (op A) (𝟙 A)) := yonedaEquiv.bijective
yoneda_fully_faithfultheoremApplies a library theorempropext, Classical.choice, Quot.sound
yoneda_fully_faithfulLean 4Applies a library theoremFormally verified
/-- **The Yoneda embedding `C ⥤ [Cᵒᵖ, Set]` is full and faithful**: `f ↦ yoneda.map f` is abijection `Hom(A, B) ≃ Nat(Hom(−, A), Hom(−, B))`. This applies Mathlib's`Yoneda.fullyFaithful` and `FullyFaithful.map_bijective`. -/theorem yoneda_fully_faithful (A B : C) : Function.Bijective (yoneda.map : (A ⟶ B) → (yoneda.obj A ⟶ yoneda.obj B)) := Yoneda.fullyFaithful.map_bijective A B
iso_of_representable_isotheoremApplies a library theorempropext, Classical.choice, Quot.sound
iso_of_representable_isoLean 4Applies a library theoremFormally verified
/-- **An object is determined by the arrows into it**: `Hom(−, A) ≅ Hom(−, B)` implies`A ≅ B`. This applies Mathlib's `FullyFaithful.preimageIso` to the Yoneda embedding. -/theorem iso_of_representable_iso {A B : C} (e : yoneda.obj A ≅ yoneda.obj B) : Nonempty (A ≅ B) := ⟨Yoneda.fullyFaithful.preimageIso e⟩
densitytheoremApplies a library theorempropext, Classical.choice, Quot.sound
densityLean 4Applies a library theoremFormally verified
/-- **Density: every presheaf is a colimit of representables.** For `P : Cᵒᵖ ⥤ Type`, thecocone over all representables `Hom(−, A) ⟶ P` with apex `P` is a colimit cocone. This appliesMathlib's `Presheaf.isColimitTautologicalCocone` (Kashiwara–Schapira, Prop. 2.6.3). -/theorem density (P : Cᵒᵖ ⥤ Type v) : Nonempty (Limits.IsColimit (Presheaf.tautologicalCocone P)) := ⟨Presheaf.isColimitTautologicalCocone P⟩
/-- The Cayley map `G → Sym(G)`, `g ↦ (x ↦ g x)` (Mathlib's `Equiv.mulLeft g`). It is theYoneda embedding of the one-object category of `G`: arrow `g` goes to "compose with `g`". -/def cayley : G →* Equiv.Perm G where toFun g := Equiv.mulLeft g map_one' := by ext x simp map_mul' g h := by ext x simp
cayley_injectivetheoremProved here from basic factspropext, Classical.choice, Quot.sound
cayley_injectiveLean 4Proved here from basic factsFormally verified
/-- **Cayley's theorem**: the Cayley map is injective, so every group is isomorphic to a groupof permutations (its image). Evaluate at `1`: if `g · 1 = h · 1` then `g = h` — the faithfulhalf of Yoneda, "a transformation is determined by where it sends the identity". -/theorem cayley_injective : Function.Injective (cayley : G →* Equiv.Perm G) := by intro g h hgh have h1 : cayley g 1 = cayley h 1 := by rw [hgh] simpa [cayley] using h1
equivariant_eq_cayleytheoremProved here from basic factspropext, Classical.choice, Quot.sound
equivariant_eq_cayleyLean 4Proved here from basic factsFormally verified
/-- **The full half: the image of Cayley's map is exactly the equivariant permutations.**A permutation `σ` of `G` that commutes with every right multiplication(`σ (x h) = σ(x) h` — a natural transformation of the representable functor of the one-objectcategory) is left multiplication by `σ(1)`: `σ(x) = σ(1 · x) = σ(1) x`. -/theorem equivariant_eq_cayley (σ : Equiv.Perm G) (hσ : ∀ x h : G, σ (x * h) = σ x * h) : σ = cayley (σ 1) := by ext x calc σ x = σ (1 * x) := by rw [one_mul] _ = σ 1 * x := hσ 1 x _ = cayley (σ 1) x := rfl
cayley_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
cayley_libraryLean 4Applies a library theoremFormally verified
/-- Cayley's theorem from Mathlib: `G` is isomorphic to a subgroup of the permutations of `G`.This applies Mathlib's `Equiv.Perm.subgroupOfMulAction` for the faithful action of `G` onitself by left multiplication. -/theorem cayley_library : Nonempty (G ≃* (MulAction.toPermHom G G).range) := ⟨Equiv.Perm.subgroupOfMulAction G G⟩
le_iff_forall_letheoremProved here from basic factsNo axioms
le_iff_forall_leLean 4Proved here from basic factsFormally verified
/-- **Yoneda for preorders.** In a preorder (a category with at most one arrow between twoobjects), `x ≤ y` exactly when everything below `x` is below `y`: "`Hom(−, x) ⇒ Hom(−, y)`exists iff `Hom(x, y)` is inhabited". Forwards by transitivity; backwards apply the hypothesisto `z = x` (the identity `x ≤ x`). -/theorem le_iff_forall_le [Preorder P] (x y : P) : x ≤ y ↔ ∀ z, z ≤ x → z ≤ y := ⟨fun hxy _ hzx => le_trans hzx hxy, fun h => h x (le_refl x)⟩
eq_of_same_lowertheoremProved here from basic factsNo axioms
eq_of_same_lowerLean 4Proved here from basic factsFormally verified
/-- **The Yoneda principle for partial orders**: if exactly the same elements lie below `x` andbelow `y`, then `x = y`. (Mathlib has this as `eq_of_forall_le_iff`.) -/theorem eq_of_same_lower [PartialOrder P] {x y : P} (h : ∀ z, z ≤ x ↔ z ≤ y) : x = y := le_antisymm ((h x).1 (le_refl x)) ((h y).2 (le_refl y))
/-- The Yoneda principle for partial orders: if exactly the same elements lie below `x` andbelow `y`, then `x = y`. Hint: apply the hypothesis to `z = x` and to `z = y`, then use`le_antisymm`. -/theorem eq_of_same_lower {P : Type*} [PartialOrder P] {x y : P} (h : ∀ z, z ≤ x ↔ z ≤ y) : x = y := by sorry
Show the compiled solution
eq_of_same_lowerLean 4Proved here from basic factsFormally verified
/-- **The Yoneda principle for partial orders**: if exactly the same elements lie below `x` andbelow `y`, then `x = y`. (Mathlib has this as `eq_of_forall_le_iff`.) -/theorem eq_of_same_lower [PartialOrder P] {x y : P} (h : ∀ z, z ≤ x ↔ z ≤ y) : x = y := le_antisymm ((h x).1 (le_refl x)) ((h y).2 (le_refl y))
/-- Cayley, the Yoneda way: a function on a group that commutes with every rightmultiplication is left multiplication by its value at `1`. Hint: `x = 1 * x`. -/theorem equivariant_eq_mul_left {G : Type*} [Group G] (σ : G → G) (hσ : ∀ x h : G, σ (x * h) = σ x * h) (x : G) : σ x = σ 1 * x := by sorry
Show the compiled solution
equivariant_eq_cayleyLean 4Proved here from basic factsFormally verified
/-- **The full half: the image of Cayley's map is exactly the equivariant permutations.**A permutation `σ` of `G` that commutes with every right multiplication(`σ (x h) = σ(x) h` — a natural transformation of the representable functor of the one-objectcategory) is left multiplication by `σ(1)`: `σ(x) = σ(1 · x) = σ(1) x`. -/theorem equivariant_eq_cayley (σ : Equiv.Perm G) (hσ : ∀ x h : G, σ (x * h) = σ x * h) : σ = cayley (σ 1) := by ext x calc σ x = σ (1 * x) := by rw [one_mul] _ = σ 1 * x := hσ 1 x _ = cayley (σ 1) x := rfl