/-- The **pairing** `⟨f, g⟩ : X → A × B` of `f : X → A` and `g : X → B` sends `x` to theordered pair `(f x, g x)`. -/def pair {X A B : Type u} (f : X → A) (g : X → B) : X → A × B := fun x => (f x, g x)
fst_comp_pairtheoremProved here from basic factsNo axioms
fst_comp_pairLean 4Proved here from basic factsFormally verified
/-- First projection after pairing gives back `f`: `π₁ ∘ ⟨f, g⟩ = f`. Both sides send `x` to`f x`, so Lean accepts `rfl` ("true by computation"). -/theorem fst_comp_pair {X A B : Type u} (f : X → A) (g : X → B) : Prod.fst ∘ pair f g = f := rfl
snd_comp_pairtheoremProved here from basic factsNo axioms
snd_comp_pairLean 4Proved here from basic factsFormally verified
/-- Second projection after pairing gives back `g`: `π₂ ∘ ⟨f, g⟩ = g`. -/theorem snd_comp_pair {X A B : Type u} (f : X → A) (g : X → B) : Prod.snd ∘ pair f g = g := rfl
pair_uniquetheoremProved here from basic factsQuot.sound
pair_uniqueLean 4Proved here from basic factsFormally verified
/-- **Uniqueness.** If `h : X → A × B` satisfies `π₁ ∘ h = f` and `π₂ ∘ h = g`, then`h = ⟨f, g⟩`. Proof, as in the lesson: for each `x`, the pair `h x` has first coordinate`f x` and second coordinate `g x`, and a pair is determined by its two coordinates(`Prod.ext`). -/theorem pair_unique {X A B : Type u} {f : X → A} {g : X → B} (h : X → A × B) (h₁ : Prod.fst ∘ h = f) (h₂ : Prod.snd ∘ h = g) : h = pair f g := by funext x apply Prod.ext · -- first coordinates: `(h x).1 = f x` exact congrFun h₁ x · -- second coordinates: `(h x).2 = g x` exact congrFun h₂ x
/-- Functions `X → A × B` correspond one-to-one with pairs of functions `(X → A, X → B)`.Forward: compose with the two projections. Backward: pair. The two round trips are theidentity: one by `fst_comp_pair`/`snd_comp_pair`, the other by `pair_unique`. -/def mapsIntoProdEquiv (X A B : Type u) : (X → A × B) ≃ (X → A) × (X → B) where toFun h := (Prod.fst ∘ h, Prod.snd ∘ h) invFun fg := pair fg.1 fg.2 left_inv h := (pair_unique h rfl rfl).symm right_inv _ := rfl
mapsIntoProdEquivLibrarydefApplies a library theoremNo axioms
mapsIntoProdEquivLibraryLean 4Applies a library theoremFormally verified
/-- Mathlib already has this correspondence, for dependent functions too:`Equiv.arrowProdEquivProdArrow`. Here we just specialise it to ordinary functions. -/def mapsIntoProdEquivLibrary (X A B : Type u) : (X → A × B) ≃ (X → A) × (X → B) := Equiv.arrowProdEquivProdArrow X (fun _ => A) (fun _ => B)
card_maps_into_prodtheoremProved here from basic factspropext, Classical.choice, Quot.sound
card_maps_into_prodLean 4Proved here from basic factsFormally verified
/-- **Counting.** For finite types, `|A × B|^|X| = |A|^|X| · |B|^|X|`. The left side countsfunctions `X → A × B`, the right side counts pairs of functions, and `mapsIntoProdEquiv`matches them up one-to-one. -/theorem card_maps_into_prod (X A B : Type u) [Fintype X] [DecidableEq X] [Fintype A] [Fintype B] : Fintype.card (A × B) ^ Fintype.card X = Fintype.card A ^ Fintype.card X * Fintype.card B ^ Fintype.card X := by calc Fintype.card (A × B) ^ Fintype.card X = Fintype.card (X → A × B) := Fintype.card_fun.symm _ = Fintype.card ((X → A) × (X → B)) := Fintype.card_congr (mapsIntoProdEquiv X A B) _ = Fintype.card (X → A) * Fintype.card (X → B) := Fintype.card_prod _ _ _ = Fintype.card A ^ Fintype.card X * Fintype.card B ^ Fintype.card X := by rw [Fintype.card_fun, Fintype.card_fun]
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor
IsProductdefDefinitionNo axioms
IsProductLean 4Formally verified
/-- `IsProduct p q` says that the type `P` with maps `p : P → A` and `q : P → B` has the**universal property of the product**: for every type `X` and every pair of maps`f : X → A`, `g : X → B` there is **exactly one** `h : X → P` with `p ∘ h = f` and`q ∘ h = g`. (`∃!` is Lean's "there exists exactly one".) -/def IsProduct {A B P : Type u} (p : P → A) (q : P → B) : Prop := ∀ (X : Type u) (f : X → A) (g : X → B), ∃! h : X → P, p ∘ h = f ∧ q ∘ h = g
prod_isProducttheoremProved here from basic factsQuot.sound
prod_isProductLean 4Proved here from basic factsFormally verified
/-- The set of ordered pairs `A × B`, with its two projections, has the universal property:existence is the pairing `⟨f, g⟩`, uniqueness is `pair_unique`. -/theorem prod_isProduct (A B : Type u) : IsProduct (Prod.fst : A × B → A) Prod.snd := by intro X f g refine ⟨pair f g, ⟨fst_comp_pair f g, snd_comp_pair f g⟩, ?_⟩ rintro h ⟨h₁, h₂⟩ exact pair_unique h h₁ h₂
swap_isProducttheoremProved here from basic factsQuot.sound
swap_isProductLean 4Proved here from basic factsFormally verified
/-- A *different* type can be a product of `A` and `B`: `B × A`, with the first map readingoff the **second** coordinate and the second map the **first**. Given `f` and `g`, the uniquecompatible map is `x ↦ (g x, f x)`. -/theorem swap_isProduct (A B : Type u) : IsProduct (Prod.snd : B × A → A) Prod.fst := by intro X f g refine ⟨fun x => (g x, f x), ⟨rfl, rfl⟩, ?_⟩ rintro h ⟨h₁, h₂⟩ funext x exact Prod.ext (congrFun h₂ x) (congrFun h₁ x)
eq_id_of_isProducttheoremProved here from basic factsNo axioms
eq_id_of_isProductLean 4Proved here from basic factsFormally verified
/-- **The key trick.** If `(P, p, q)` is a product and `k : P → P` is compatible with the maps(`p ∘ k = p` and `q ∘ k = q`), then `k` is the identity. Reason: apply the universal propertywith `X = P`, `f = p`, `g = q`. Both `k` and `id` are compatible maps, and there is only one. -/theorem eq_id_of_isProduct {A B P : Type u} {p : P → A} {q : P → B} (hP : IsProduct p q) (k : P → P) (hk₁ : p ∘ k = p) (hk₂ : q ∘ k = q) : k = id := by obtain ⟨_, _, huniq⟩ := hP P p q have hk : k = _ := huniq k ⟨hk₁, hk₂⟩ have hid : id = _ := huniq id ⟨rfl, rfl⟩ exact hk.trans hid.symm
isProduct_bijectivetheoremProved here from basic factspropext, Classical.choice, Quot.sound
isProduct_bijectiveLean 4Proved here from basic factsFormally verified
/-- **A product is determined up to a unique compatible bijection.** If `(P, p, q)` has theuniversal property, then `⟨p, q⟩ : P → A × B` is a bijection. (It is compatible with the mapsby `fst_comp_pair`/`snd_comp_pair`, and it is the *only* compatible map by `pair_unique`.)Proof, as in the lesson. The universal property of `P`, applied to the projections of `A × B`,gives `ψ : A × B → P` with `p ∘ ψ = π₁` and `q ∘ ψ = π₂`. Then `ψ ∘ ⟨p, q⟩ : P → P` iscompatible with `p` and `q`, so it is the identity by `eq_id_of_isProduct`; and`⟨p, q⟩ ∘ ψ : A × B → A × B` is compatible with the projections, so it is the identity by`pair_unique`. A map with a two-sided inverse is a bijection. -/theorem isProduct_bijective {A B P : Type u} {p : P → A} {q : P → B} (hP : IsProduct p q) : Function.Bijective (pair p q) := by obtain ⟨ψ, ⟨hψ₁, hψ₂⟩, _⟩ := hP (A × B) (Prod.fst : A × B → A) (Prod.snd : A × B → B) rw [Function.bijective_iff_has_inverse] refine ⟨ψ, ?_, ?_⟩ · -- `ψ ∘ ⟨p, q⟩ = id` on `P` have h : ψ ∘ pair p q = id := by apply eq_id_of_isProduct hP · calc p ∘ (ψ ∘ pair p q) = (p ∘ ψ) ∘ pair p q := rfl _ = Prod.fst ∘ pair p q := by rw [hψ₁] _ = p := fst_comp_pair p q · calc q ∘ (ψ ∘ pair p q) = (q ∘ ψ) ∘ pair p q := rfl _ = Prod.snd ∘ pair p q := by rw [hψ₂] _ = q := snd_comp_pair p q exact congrFun h · -- `⟨p, q⟩ ∘ ψ = id` on `A × B` have h : pair p q ∘ ψ = id := by have hu : pair p q ∘ ψ = pair (Prod.fst : A × B → A) (Prod.snd : A × B → B) := pair_unique (pair p q ∘ ψ) hψ₁ hψ₂ rw [hu] rfl exact congrFun h
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor
not_isProduct_emptytheoremProved here from basic factsNo axioms
not_isProduct_emptyLean 4Proved here from basic factsFormally verified
/-- **Existence can fail.** Take `A = B = Unit` (one element each) and `P = Empty`. There is nomap at all from `Unit` to `Empty`, so the pair of maps `Unit → Unit` cannot factor through `P`. -/theorem not_isProduct_empty : ¬ IsProduct (fun e : Empty => (Empty.elim e : Unit)) (fun e : Empty => (Empty.elim e : Unit)) := by intro hP obtain ⟨h, _, _⟩ := hP Unit id id exact (h ()).elim
not_isProduct_booltheoremProved here from basic factsNo axioms
not_isProduct_boolLean 4Proved here from basic factsFormally verified
/-- **Uniqueness can fail.** Take `A = B = Unit` and `P = Bool` (two elements), with the onlypossible maps `P → Unit`. Then *both* constant maps `Unit → Bool` are compatible, so there isnot exactly one. The universal property needs its "exactly". -/theorem not_isProduct_bool : ¬ IsProduct (fun _ : Bool => ()) (fun _ : Bool => ()) := by intro hP obtain ⟨_, _, huniq⟩ := hP Unit id id have ht : (fun _ : Unit => true) = _ := huniq (fun _ => true) ⟨rfl, rfl⟩ have hf : (fun _ : Unit => false) = _ := huniq (fun _ => false) ⟨rfl, rfl⟩ have h : (fun _ : Unit => true) = (fun _ : Unit => false) := ht.trans hf.symm exact Bool.noConfusion (congrFun h ())
/-- A function into `A × B` is determined by its two components.Hint: `funext x` reduces the goal to one point; then `Prod.ext` splits it into the twocoordinates, and `congrFun h₁ x` turns `h₁ : Prod.fst ∘ h = f` into `(h x).1 = f x`. -/theorem pair_unique {X A B : Type u} {f : X → A} {g : X → B} (h : X → A × B) (h₁ : Prod.fst ∘ h = f) (h₂ : Prod.snd ∘ h = g) : h = pair f g := by sorry
Show the compiled solution
pair_uniqueLean 4Proved here from basic factsFormally verified
/-- **Uniqueness.** If `h : X → A × B` satisfies `π₁ ∘ h = f` and `π₂ ∘ h = g`, then`h = ⟨f, g⟩`. Proof, as in the lesson: for each `x`, the pair `h x` has first coordinate`f x` and second coordinate `g x`, and a pair is determined by its two coordinates(`Prod.ext`). -/theorem pair_unique {X A B : Type u} {f : X → A} {g : X → B} (h : X → A × B) (h₁ : Prod.fst ∘ h = f) (h₂ : Prod.snd ∘ h = g) : h = pair f g := by funext x apply Prod.ext · -- first coordinates: `(h x).1 = f x` exact congrFun h₁ x · -- second coordinates: `(h x).2 = g x` exact congrFun h₂ x
/-- `B × A`, with the maps reading off the second and the first coordinate, is a product of`A` and `B`. Hint: start with `intro X f g`, and offer `fun x => (g x, f x)` as the map. -/theorem swap_isProduct (A B : Type u) : IsProduct (Prod.snd : B × A → A) Prod.fst := by sorry
Show the compiled solution
swap_isProductLean 4Proved here from basic factsFormally verified
/-- A *different* type can be a product of `A` and `B`: `B × A`, with the first map readingoff the **second** coordinate and the second map the **first**. Given `f` and `g`, the uniquecompatible map is `x ↦ (g x, f x)`. -/theorem swap_isProduct (A B : Type u) : IsProduct (Prod.snd : B × A → A) Prod.fst := by intro X f g refine ⟨fun x => (g x, f x), ⟨rfl, rfl⟩, ?_⟩ rintro h ⟨h₁, h₂⟩ funext x exact Prod.ext (congrFun h₂ x) (congrFun h₁ x)