/-- **The universal property of a product.** Projections `π₁ : P ⟶ A` and `π₂ : P ⟶ B` make `P`a product of `A` and `B` when every pair `f : X ⟶ A`, `g : X ⟶ B` factors through `P` by exactlyone morphism `lift f g : X ⟶ P`. Mathlib composes in diagrammatic order: `h ≫ π₁` means"first `h`, then `π₁`", i.e. `π₁ ∘ h`. -/structure IsBinaryProduct {A B P : C} (π₁ : P ⟶ A) (π₂ : P ⟶ B) where /-- The induced morphism `⟨f, g⟩ : X ⟶ P`. -/ lift : ∀ {X : C}, (X ⟶ A) → (X ⟶ B) → (X ⟶ P) /-- `π₁ ∘ ⟨f, g⟩ = f`. -/ lift_fst : ∀ {X : C} (f : X ⟶ A) (g : X ⟶ B), lift f g ≫ π₁ = f /-- `π₂ ∘ ⟨f, g⟩ = g`. -/ lift_snd : ∀ {X : C} (f : X ⟶ A) (g : X ⟶ B), lift f g ≫ π₂ = g /-- Uniqueness: any `h` with `π₁ ∘ h = f` and `π₂ ∘ h = g` is `⟨f, g⟩`. -/ uniq : ∀ {X : C} (f : X ⟶ A) (g : X ⟶ B) (h : X ⟶ P), h ≫ π₁ = f → h ≫ π₂ = g → h = lift f g
IsBinaryProduct.hom_exttheoremProved here from basic factsNo axioms
hom_extLean 4Proved here from basic factsFormally verified
/-- **Morphisms into a product are determined by their components.** If `h` and `k` agree afterboth projections, both equal `lift (h ≫ π₁) (h ≫ π₂)` by the uniqueness clause. -/theorem hom_ext (hP : IsBinaryProduct π₁ π₂) {X : C} {h k : X ⟶ P} (h₁ : h ≫ π₁ = k ≫ π₁) (h₂ : h ≫ π₂ = k ≫ π₂) : h = k := by rw [hP.uniq _ _ h rfl rfl, hP.uniq _ _ k h₁.symm h₂.symm]
IsBinaryProduct.iso_uniquetheoremProved here from basic factspropext, Classical.choice, Quot.sound
iso_uniqueLean 4Proved here from basic factsFormally verified
/-- **…by a unique isomorphism compatible with the projections.** Any isomorphism `i : P ≅ Q`with `ρ₁ ∘ i = π₁` and `ρ₂ ∘ i = π₂` is the comparison isomorphism `iso hP hQ`: its forward mapsatisfies the defining equations of `lift π₁ π₂`, so uniqueness in `Q`'s universal propertyidentifies them (and an isomorphism is determined by its forward map). -/theorem iso_unique (hP : IsBinaryProduct π₁ π₂) (hQ : IsBinaryProduct ρ₁ ρ₂) (i : P ≅ Q) (h₁ : i.hom ≫ ρ₁ = π₁) (h₂ : i.hom ≫ ρ₂ = π₂) : i = iso hP hQ := by ext exact hQ.uniq π₁ π₂ i.hom h₁ h₂
/-- **Mathlib's products satisfy our universal property.** When `A` and `B` have a (chosen)product `A ⨯ B` in Mathlib, its projections `prod.fst`, `prod.snd` form an `IsBinaryProduct`;the induced map is Mathlib's `prod.lift`, and uniqueness is `prod.hom_ext`. -/noncomputable def ofHasBinaryProduct (A B : C) [HasBinaryProduct A B] : IsBinaryProduct (prod.fst : A ⨯ B ⟶ A) prod.snd where lift f g := prod.lift f g lift_fst f g := prod.lift_fst f g lift_snd f g := prod.lift_snd f g uniq f g h h₁ h₂ := prod.hom_ext (by rw [h₁, prod.lift_fst]) (by rw [h₂, prod.lift_snd])
product_is_terminal_conetheoremApplies a library theorempropext, Classical.choice, Quot.sound
product_is_terminal_coneLean 4Applies a library theoremFormally verified
/-- **A product is a terminal cone.** A cone over the pair `(A, B)` is an object with two maps to`A` and `B` (a `BinaryFan`); cones and their morphisms form a category, and a cone is a limit —here, a product — exactly when it is a terminal object of that category. This applies Mathlib's`Cone.isLimitEquivIsTerminal`. -/theorem product_is_terminal_cone {A B : C} (c : BinaryFan A B) : Nonempty (IsLimit c) ↔ Nonempty (IsTerminal c) := ⟨fun ⟨h⟩ => ⟨Cone.isLimitEquivIsTerminal c h⟩, fun ⟨h⟩ => ⟨(Cone.isLimitEquivIsTerminal c).symm h⟩⟩
/-- **A coproduct in `C` is a product in `Cᵒᵖ`.** Injections `ι₁ : A ⟶ S`, `ι₂ : B ⟶ S` make`S` a coproduct of `A` and `B` when the reversed arrows `ι₁.op : op S ⟶ op A`,`ι₂.op : op S ⟶ op B` make `op S` a product of `op A` and `op B` in the opposite category.This *is* the definition — duality is built in. -/abbrev IsBinaryCoproduct {A B S : C} (ι₁ : A ⟶ S) (ι₂ : B ⟶ S) : Type _ := IsBinaryProduct ι₁.op ι₂.op
/-- **Unpacking the dual definition: copairing.** Maps `f : A ⟶ Y` and `g : B ⟶ Y` in `C` aremaps `op Y ⟶ op A` and `op Y ⟶ op B` in `Cᵒᵖ`; the product property gives `op Y ⟶ op S`, i.e. amap `[f, g] : S ⟶ Y` in `C`. -/def desc (hS : IsBinaryCoproduct ι₁ ι₂) {Y : C} (f : A ⟶ Y) (g : B ⟶ Y) : S ⟶ Y := (hS.lift f.op g.op).unop
terminal_uniquetheoremProved here from basic factspropext, Classical.choice, Quot.sound
terminal_uniqueLean 4Proved here from basic factsFormally verified
/-- **Terminal objects are unique up to unique isomorphism.** If `T` and `T'` are terminal, theunique maps `T ⟶ T'` and `T' ⟶ T` compose to endomorphisms of a terminal object, which must beidentities because a terminal object has only one endomorphism. (Mathlib: `IsTerminal.uniqueUpToIso`.)Dually for initial objects. -/theorem terminal_unique {T T' : C} (hT : IsTerminal T) (hT' : IsTerminal T') : ∃ i : T ≅ T', ∀ j : T ≅ T', j = i := ⟨⟨hT'.from T, hT.from T', hT.hom_ext _ _, hT'.hom_ext _ _⟩, fun _ => Iso.ext (hT'.hom_ext _ _)⟩
/-- **In the category of types, the product is the type of pairs.** Given `f : X → A` and`g : X → B`, the unique map `X → A × B` compatible with the projections is`x ↦ (f x, g x)`: any compatible `h` has first and second coordinates `f x` and `g x`. -/def typesProduct (A B : Type u) : IsBinaryProduct (C := Type u) (↾(Prod.fst : A × B → A)) (↾(Prod.snd : A × B → B)) where lift f g := ↾fun x => (f x, g x) lift_fst _ _ := rfl lift_snd _ _ := rfl uniq f g h h₁ h₂ := by -- `ext` reduces to the two coordinates of `h x`. ext x · simpa using ConcreteCategory.congr_hom h₁ x · simpa using ConcreteCategory.congr_hom h₂ x
/-- **In the category of types, the coproduct is the disjoint union** `A ⊕ B`, with theinjections `Sum.inl`, `Sum.inr`. Following the definition, we exhibit a product in `(Type u)ᵒᵖ`:the induced map is "case analysis" `Sum.elim f g`, and it is unique because a function on`A ⊕ B` is determined by its values on the two summands. -/def typesCoproduct (A B : Type u) : IsBinaryCoproduct (C := Type u) (↾(Sum.inl : A → A ⊕ B)) (↾(Sum.inr : B → A ⊕ B)) where lift f g := (↾(Sum.elim f.unop g.unop)).op lift_fst _ _ := rfl lift_snd _ _ := rfl uniq f g h h₁ h₂ := by apply Quiver.Hom.unop_inj ext x rcases x with a | b · exact ConcreteCategory.congr_hom (congrArg Quiver.Hom.unop h₁) a · exact ConcreteCategory.congr_hom (congrArg Quiver.Hom.unop h₂) b
types_terminal_initialtheoremApplies a library theorempropext, Classical.choice, Quot.sound
types_terminal_initialLean 4Applies a library theoremFormally verified
/-- **In the category of types, a one-element type is terminal and the empty type is initial.**Every type has exactly one map to `PUnit` and exactly one map from `PEmpty`. These are Mathlib's`Types.isTerminalPUnit` and `Types.isInitialPEmpty`. -/theorem types_terminal_initial : Nonempty (IsTerminal (PUnit : Type u)) ∧ Nonempty (IsInitial (PEmpty : Type u)) := ⟨⟨Types.isTerminalPUnit⟩, ⟨Types.isInitialPEmpty⟩⟩
/-- **In a poset regarded as a category, the product is the meet.** There is a morphism `x ⟶ y`exactly when `x ≤ y`, and then only one, so the equations in the universal property areautomatic; what remains is existence: `x ≤ a` and `x ≤ b` imply `x ≤ a ⊓ b`. -/def infIsProduct [SemilatticeInf α] (a b : α) : IsBinaryProduct (homOfLE (inf_le_left : a ⊓ b ≤ a)) (homOfLE inf_le_right) where lift f g := homOfLE (le_inf (leOfHom f) (leOfHom g)) lift_fst _ _ := Subsingleton.elim _ _ lift_snd _ _ := Subsingleton.elim _ _ uniq _ _ _ _ _ := Subsingleton.elim _ _
product_eq_inftheoremProved here from basic factsNo axioms
product_eq_infLean 4Proved here from basic factsFormally verified
/-- **Conversely, every product in a poset is the meet.** If `p` (with `p ≤ a`, `p ≤ b`) is aproduct of `a` and `b`, then `p ≤ a ⊓ b` because `a ⊓ b` is a lower bound, and `a ⊓ b ≤ p` bythe universal property applied to the cone `a ⊓ b`. Antisymmetry gives `p = a ⊓ b`. So a pairwith no greatest lower bound has no product. -/theorem product_eq_inf [SemilatticeInf α] {a b p : α} {π₁ : p ⟶ a} {π₂ : p ⟶ b} (hp : IsBinaryProduct π₁ π₂) : p = a ⊓ b := le_antisymm (le_inf (leOfHom π₁) (leOfHom π₂)) (leOfHom (hp.lift (homOfLE inf_le_left) (homOfLE inf_le_right)))
int_initialtheoremApplies a library theorempropext, Classical.choice, Quot.sound
int_initialLean 4Applies a library theoremFormally verified
/-- **`ℤ` is initial among commutative rings**: for every commutative ring `R` there is exactly onering homomorphism `ℤ → R`, namely `n ↦ n · 1`. This is Mathlib's `CommRingCat.zIsInitial`(uniqueness is `RingHom.ext_int`). -/theorem int_initial : Nonempty (IsInitial (CommRingCat.of ℤ)) := ⟨CommRingCat.zIsInitial⟩
trivial_group_zerotheoremApplies a library theorempropext, Quot.sound
trivial_group_zeroLean 4Applies a library theoremFormally verified
/-- **The trivial group is both initial and terminal in `Grp`** (a *zero object*): from any groupthere is one homomorphism to it, and to any group there is one homomorphism from it (sending theidentity to the identity). This applies Mathlib's `GrpCat.isZero_of_subsingleton`. -/theorem trivial_group_zero : IsZero (GrpCat.of PUnit) := GrpCat.isZero_of_subsingleton _
free_product_not_commtheoremProved here from basic factspropext, Classical.choice, Quot.sound
free_product_not_commLean 4Proved here from basic factsFormally verified
/-- **`ℤ ∗ ℤ` is not commutative.** In `Grp`, the coproduct of `ℤ` with itself is the free product`ℤ ∗ ℤ` (Mathlib's `Monoid.Coprod`, written multiplicatively). Let `x` and `y` be the generators ofthe two copies. By the universal property there is a homomorphism `φ : ℤ ∗ ℤ → S₃` sending `x` tothe transposition `(0 1)` and `y` to `(1 2)`. If `x y = y x`, then `φ` would make these twotranspositions commute, and they do not (checked by `decide`). Contrast `prod_comm`. -/theorem free_product_not_comm : ∃ x y : Multiplicative ℤ ∗ Multiplicative ℤ, x * y ≠ y * x := by refine ⟨Monoid.Coprod.inl (Multiplicative.ofAdd 1), Monoid.Coprod.inr (Multiplicative.ofAdd 1), fun h => ?_⟩ -- The homomorphism given by the universal property of the coproduct. let φ := Monoid.Coprod.lift (zpowersHom (Equiv.Perm (Fin 3)) (Equiv.swap 0 1)) (zpowersHom (Equiv.Perm (Fin 3)) (Equiv.swap 1 2)) have hφ := congrArg φ h simp only [φ, map_mul, Monoid.Coprod.lift_apply_inl, Monoid.Coprod.lift_apply_inr, zpowersHom_apply, toAdd_ofAdd, zpow_one] at hφ exact absurd hφ (by decide)
prod_commtheoremProved here from basic factspropext, Quot.sound
prod_commLean 4Proved here from basic factsFormally verified
/-- **`ℤ × ℤ` is commutative**: the product of two abelian groups is abelian, componentwise. So theproduct and the coproduct of `ℤ` with itself in `Grp` are genuinely different groups. -/theorem prod_comm (x y : Multiplicative ℤ × Multiplicative ℤ) : x * y = y * x := Prod.ext (mul_comm x.1 y.1) (mul_comm x.2 y.2)
/-- Two morphisms into a product that agree after both projections are equal.Hint: the uniqueness clause `hP.uniq f g h h₁ h₂` says any `h` with `h ≫ π₁ = f` and`h ≫ π₂ = g` equals `hP.lift f g`. Apply it to `h` and to `k` with the same `f` and `g`(take `f := h ≫ π₁`, `g := h ≫ π₂`), then rewrite. -/theorem hom_ext {C : Type u} [Category.{v} C] {A B P : C} {π₁ : P ⟶ A} {π₂ : P ⟶ B} (hP : IsBinaryProduct π₁ π₂) {X : C} {h k : X ⟶ P} (h₁ : h ≫ π₁ = k ≫ π₁) (h₂ : h ≫ π₂ = k ≫ π₂) : h = k := by sorry
Show the compiled solution
hom_extLean 4Proved here from basic factsFormally verified
/-- **Morphisms into a product are determined by their components.** If `h` and `k` agree afterboth projections, both equal `lift (h ≫ π₁) (h ≫ π₂)` by the uniqueness clause. -/theorem hom_ext (hP : IsBinaryProduct π₁ π₂) {X : C} {h k : X ⟶ P} (h₁ : h ≫ π₁ = k ≫ π₁) (h₂ : h ≫ π₂ = k ≫ π₂) : h = k := by rw [hP.uniq _ _ h rfl rfl, hP.uniq _ _ k h₁.symm h₂.symm]
/-- In a poset, a product of `a` and `b` is their meet.Hint: use `le_antisymm`. One inequality is `le_inf (leOfHom π₁) (leOfHom π₂)`; for the other,apply the universal property `hp.lift` to the two morphisms `homOfLE inf_le_left` and`homOfLE inf_le_right` out of `a ⊓ b`, and turn the result into an inequality with `leOfHom`. -/theorem product_eq_inf {α : Type u} [SemilatticeInf α] {a b p : α} {π₁ : p ⟶ a} {π₂ : p ⟶ b} (hp : IsBinaryProduct π₁ π₂) : p = a ⊓ b := by sorry
Show the compiled solution
product_eq_infLean 4Proved here from basic factsFormally verified
/-- **Conversely, every product in a poset is the meet.** If `p` (with `p ≤ a`, `p ≤ b`) is aproduct of `a` and `b`, then `p ≤ a ⊓ b` because `a ⊓ b` is a lower bound, and `a ⊓ b ≤ p` bythe universal property applied to the cone `a ⊓ b`. Antisymmetry gives `p = a ⊓ b`. So a pairwith no greatest lower bound has no product. -/theorem product_eq_inf [SemilatticeInf α] {a b p : α} {π₁ : p ⟶ a} {π₂ : p ⟶ b} (hp : IsBinaryProduct π₁ π₂) : p = a ⊓ b := le_antisymm (le_inf (leOfHom π₁) (leOfHom π₂)) (leOfHom (hp.lift (homOfLE inf_le_left) (homOfLE inf_le_right)))