Session 27: Examples of universal constructions
2. Can objects have negatives?
Exercise 1 (p. 288)
Prove that if A and B are objects and {A \times B = \mathbf{1}}, then {A = B = \mathbf{1}}. More precisely, if \mathbf{1} is terminal and
A \xleftarrow{p_1} \mathbf{1} \xrightarrow{p_2} B
is a product, then A and B are terminal objects.
Solution: Exercise 1
To prove that A and B are terminal, we construct two binary fans over A and B, one with vertex A and the other with vertex B. The universal property of the product yields a unique map from each vertex to the limit \mathbf{1}. We then use the universal properties of product and terminal object to show that these maps form isomorphisms.
example {π : Type u} [Category.{v, u} π] [HasTerminal π]
(A B : π) (pβ : β€_ π βΆ A) (pβ : β€_ π βΆ B)
(P : IsLimit (BinaryFan.mk pβ pβ)) :
Nonempty (A β
β€_ π) β§ Nonempty (B β
β€_ π) := π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πA:πB:πpβ:β€_ π βΆ Apβ:β€_ π βΆ BP:IsLimit (BinaryFan.mk pβ pβ)β’ Nonempty (A β
β€_ π) β§ Nonempty (B β
β€_ π)
π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πA:πB:πpβ:β€_ π βΆ Apβ:β€_ π βΆ BP:IsLimit (BinaryFan.mk pβ pβ)β’ Nonempty (A β
β€_ π)π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πA:πB:πpβ:β€_ π βΆ Apβ:β€_ π βΆ BP:IsLimit (BinaryFan.mk pβ pβ)β’ Nonempty (B β
β€_ π) π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πA:πB:πpβ:β€_ π βΆ Apβ:β€_ π βΆ BP:IsLimit (BinaryFan.mk pβ pβ)β’ Nonempty (A β
β€_ π)π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πA:πB:πpβ:β€_ π βΆ Apβ:β€_ π βΆ BP:IsLimit (BinaryFan.mk pβ pβ)β’ Nonempty (B β
β€_ π) π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πA:πB:πpβ:β€_ π βΆ Apβ:β€_ π βΆ BP:IsLimit (BinaryFan.mk pβ pβ)β’ B β
β€_ π
π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πA:πB:πpβ:β€_ π βΆ Apβ:β€_ π βΆ BP:IsLimit (BinaryFan.mk pβ pβ)β’ A β
β€_ π π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πA:πB:πpβ:β€_ π βΆ Apβ:β€_ π βΆ BP:IsLimit (BinaryFan.mk pβ pβ)fanA:BinaryFan A B := BinaryFan.mk (π A) (pβ β terminal.from A)β’ A β
β€_ π
All goals completed! π
π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πA:πB:πpβ:β€_ π βΆ Apβ:β€_ π βΆ BP:IsLimit (BinaryFan.mk pβ pβ)β’ B β
β€_ π π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πA:πB:πpβ:β€_ π βΆ Apβ:β€_ π βΆ BP:IsLimit (BinaryFan.mk pβ pβ)fanB:BinaryFan A B := BinaryFan.mk (pβ β terminal.from B) (π B)β’ B β
β€_ π
All goals completed! π
3. Idempotent objects
Exercise 2 (p. 290)
(a) Show that if C has the property that for each X there is at most one map {X \rightarrow C}, then
C \xleftarrow{1_C} C \xrightarrow{1_C} C
is a product.
(b) Show that the property above is also equivalent to the following property: The unique map {C \rightarrow \mathbf{1}} is a monomorphism.
Solution: Exercise 2
Since in mathlib the Subsingleton type class represents a type with at most one element, we can use Subsingleton in both parts of the exercise to formalise the property that for each X there is at most one map {X \rightarrow C}.
For part (a), we have
example {π : Type u} [Category.{v, u} π] (C : π)
(h : β X : π, Subsingleton (X βΆ C)) :
IsLimit (BinaryFan.mk (π C) (π C)) := {
lift s := BinaryFan.fst s
fac s := fun β¨jβ© β¦ π:Type uinstβ:Category.{v, u} πC:πh:β (X : π), Subsingleton (X βΆ C)s:Cone (pair C C)xβ:Discrete WalkingPairj:WalkingPairβ’ (BinaryFan.mk (π C) (π C)).Ο.app { as := j } β BinaryFan.fst s = s.Ο.app { as := j }
π:Type uinstβ:Category.{v, u} πC:πh:β (X : π), Subsingleton (X βΆ C)s:Cone (pair C C)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π C) (π C)).Ο.app { as := WalkingPair.left } β BinaryFan.fst s = s.Ο.app { as := WalkingPair.left }π:Type uinstβ:Category.{v, u} πC:πh:β (X : π), Subsingleton (X βΆ C)s:Cone (pair C C)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π C) (π C)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s = s.Ο.app { as := WalkingPair.right }
all_goals
π:Type uinstβ:Category.{v, u} πC:πh:β (X : π), Subsingleton (X βΆ C)s:Cone (pair C C)xβ:Discrete WalkingPairβ’ π C β BinaryFan.fst s = s.Ο.app { as := WalkingPair.right }
All goals completed! π
uniq s m _ := π:Type uinstβ:Category.{v, u} πC:πh:β (X : π), Subsingleton (X βΆ C)s:Cone (pair C C)m:s.pt βΆ (BinaryFan.mk (π C) (π C)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π C) (π C)).Ο.app j β m = s.Ο.app jβ’ m = BinaryFan.fst s
π:Type uinstβ:Category.{v, u} πC:πh:β (X : π), Subsingleton (X βΆ C)s:Cone (pair C C)m:s.pt βΆ (BinaryFan.mk (π C) (π C)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π C) (π C)).Ο.app j β m = s.Ο.app jβ’ m = BinaryFan.fst s
All goals completed! π
}
and for part (b), we have
example {π : Type u} [Category.{v, u} π] [HasTerminal π] (C : π) :
(β X : π, Subsingleton (X βΆ C)) β Mono (terminal.from C) := π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πC:πβ’ (β (X : π), Subsingleton (X βΆ C)) β Mono (terminal.from C)
π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πC:πβ’ (β (X : π), Subsingleton (X βΆ C)) β Mono (terminal.from C)π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πC:πβ’ Mono (terminal.from C) β β (X : π), Subsingleton (X βΆ C)
π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πC:πβ’ (β (X : π), Subsingleton (X βΆ C)) β Mono (terminal.from C) π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πC:πaβ:β (X : π), Subsingleton (X βΆ C)β’ Mono (terminal.from C)
All goals completed! π
π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πC:πβ’ Mono (terminal.from C) β β (X : π), Subsingleton (X βΆ C) intro h π:Type uinstβΒΉ:Category.{v, u} πinstβ:HasTerminal πC:πh:Mono (terminal.from C)X:πβ’ Subsingleton (X βΆ C)
All goals completed! π
Exercise 3 (p. 291)
Find all objects C in πΊ, πΊβ», and πΊβ such that this is a product:
C \xleftarrow{1_C} C \xrightarrow{1_C} C
Solution: Exercise 3
In πΊ, C must either be empty or have a single elementβi.e., C must be a Subsingleton type.
example (C : Type) :
Subsingleton C β IsLimit (BinaryFan.mk (π C) (π C)) := C:Typeβ’ Subsingleton C β IsLimit (BinaryFan.mk (π C) (π C))
C:Typeaβ:Subsingleton Cβ’ IsLimit (BinaryFan.mk (π C) (π C))
exact {
lift s := BinaryFan.fst s
fac s := fun β¨jβ© β¦ C:Typeaβ:Subsingleton Cs:Cone (pair C C)xβ:Discrete WalkingPairj:WalkingPairβ’ (BinaryFan.mk (π C) (π C)).Ο.app { as := j } β BinaryFan.fst s = s.Ο.app { as := j }
C:Typeaβ:Subsingleton Cs:Cone (pair C C)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π C) (π C)).Ο.app { as := WalkingPair.left } β BinaryFan.fst s = s.Ο.app { as := WalkingPair.left }C:Typeaβ:Subsingleton Cs:Cone (pair C C)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π C) (π C)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s = s.Ο.app { as := WalkingPair.right }
all_goals
C:Typeaβ:Subsingleton Cs:Cone (pair C C)xβ:Discrete WalkingPairβ’ π C β BinaryFan.fst s = s.Ο.app { as := WalkingPair.right }
C:Typeaβ:Subsingleton Cs:Cone (pair C C)xβ:Discrete WalkingPairx:s.ptβ’ (π C β BinaryFan.fst s) x = s.Ο.app { as := WalkingPair.right } x
All goals completed! π
uniq s m _ := C:Typeaβ:Subsingleton Cs:Cone (pair C C)m:s.pt βΆ (BinaryFan.mk (π C) (π C)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π C) (π C)).Ο.app j β m = s.Ο.app jβ’ m = BinaryFan.fst s
C:Typeaβ:Subsingleton Cs:Cone (pair C C)m:s.pt βΆ (BinaryFan.mk (π C) (π C)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π C) (π C)).Ο.app j β m = s.Ο.app jx:s.ptβ’ m x = BinaryFan.fst s x
All goals completed! π
}
In πΊβ», C must either be empty or have a single element with the identity map. (We re-use relevant definitions from Article IV.)
example : IsLimit (BinaryFan.mk (π emptySWE) (π emptySWE)) := β’ IsLimit (BinaryFan.mk (π emptySWE) (π emptySWE))
exact {
lift s := BinaryFan.fst s
fac s := fun β¨jβ© β¦ s:Cone (pair emptySWE emptySWE)xβ:Discrete WalkingPairj:WalkingPairβ’ (BinaryFan.mk (π emptySWE) (π emptySWE)).Ο.app { as := j } β BinaryFan.fst s = s.Ο.app { as := j }
s:Cone (pair emptySWE emptySWE)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π emptySWE) (π emptySWE)).Ο.app { as := WalkingPair.left } β BinaryFan.fst s =
s.Ο.app { as := WalkingPair.left }s:Cone (pair emptySWE emptySWE)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π emptySWE) (π emptySWE)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s =
s.Ο.app { as := WalkingPair.right }
all_goals
s:Cone (pair emptySWE emptySWE)xβ:Discrete WalkingPairβ’ β (x : ToType s.pt),
(ConcreteCategory.hom ((BinaryFan.mk (π emptySWE) (π emptySWE)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s))
x =
(ConcreteCategory.hom (s.Ο.app { as := WalkingPair.right })) x
s:Cone (pair emptySWE emptySWE)xβ:Discrete WalkingPairx:ToType s.ptβ’ (ConcreteCategory.hom ((BinaryFan.mk (π emptySWE) (π emptySWE)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s))
x =
(ConcreteCategory.hom (s.Ο.app { as := WalkingPair.right })) x
All goals completed! π
uniq s m _ := s:Cone (pair emptySWE emptySWE)m:s.pt βΆ (BinaryFan.mk (π emptySWE) (π emptySWE)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π emptySWE) (π emptySWE)).Ο.app j β m = s.Ο.app jβ’ m = BinaryFan.fst s
s:Cone (pair emptySWE emptySWE)m:s.pt βΆ (BinaryFan.mk (π emptySWE) (π emptySWE)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π emptySWE) (π emptySWE)).Ο.app j β m = s.Ο.app jβ’ β (x : ToType s.pt), (ConcreteCategory.hom m) x = (ConcreteCategory.hom (BinaryFan.fst s)) x
s:Cone (pair emptySWE emptySWE)m:s.pt βΆ (BinaryFan.mk (π emptySWE) (π emptySWE)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π emptySWE) (π emptySWE)).Ο.app j β m = s.Ο.app jx:ToType s.ptβ’ (ConcreteCategory.hom m) x = (ConcreteCategory.hom (BinaryFan.fst s)) x
All goals completed! π
}
-- Single element with identity map (terminal object in πΊβ»)
example : IsLimit (BinaryFan.mk (π termSWE) (π termSWE)) := β’ IsLimit (BinaryFan.mk (π termSWE) (π termSWE))
exact {
lift s := BinaryFan.fst s
fac s := fun β¨jβ© β¦ s:Cone (pair termSWE termSWE)xβ:Discrete WalkingPairj:WalkingPairβ’ (BinaryFan.mk (π termSWE) (π termSWE)).Ο.app { as := j } β BinaryFan.fst s = s.Ο.app { as := j }
s:Cone (pair termSWE termSWE)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π termSWE) (π termSWE)).Ο.app { as := WalkingPair.left } β BinaryFan.fst s =
s.Ο.app { as := WalkingPair.left }s:Cone (pair termSWE termSWE)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π termSWE) (π termSWE)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s =
s.Ο.app { as := WalkingPair.right } s:Cone (pair termSWE termSWE)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π termSWE) (π termSWE)).Ο.app { as := WalkingPair.left } β BinaryFan.fst s =
s.Ο.app { as := WalkingPair.left }s:Cone (pair termSWE termSWE)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π termSWE) (π termSWE)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s =
s.Ο.app { as := WalkingPair.right } All goals completed! π
uniq s m _ := s:Cone (pair termSWE termSWE)m:s.pt βΆ (BinaryFan.mk (π termSWE) (π termSWE)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π termSWE) (π termSWE)).Ο.app j β m = s.Ο.app jβ’ m = BinaryFan.fst s
s:Cone (pair termSWE termSWE)m:s.pt βΆ (BinaryFan.mk (π termSWE) (π termSWE)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π termSWE) (π termSWE)).Ο.app j β m = s.Ο.app jβ’ β (x : ToType s.pt), (ConcreteCategory.hom m) x = (ConcreteCategory.hom (BinaryFan.fst s)) x
s:Cone (pair termSWE termSWE)m:s.pt βΆ (BinaryFan.mk (π termSWE) (π termSWE)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π termSWE) (π termSWE)).Ο.app j β m = s.Ο.app jx:ToType s.ptβ’ (ConcreteCategory.hom m) x = (ConcreteCategory.hom (BinaryFan.fst s)) x
All goals completed! π
}
In πΊβ, C must either be the empty graph, a 'naked dot', or a single dot with one looping arrow. (We again re-use relevant definitions from Article IV.)
example : IsLimit (BinaryFan.mk (π emptyIG) (π emptyIG)) := β’ IsLimit (BinaryFan.mk (π emptyIG) (π emptyIG))
exact {
lift s := BinaryFan.fst s
fac s := fun β¨jβ© β¦ s:Cone (pair emptyIG emptyIG)xβ:Discrete WalkingPairj:WalkingPairβ’ (BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app { as := j } β BinaryFan.fst s = s.Ο.app { as := j }
s:Cone (pair emptyIG emptyIG)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app { as := WalkingPair.left } β BinaryFan.fst s =
s.Ο.app { as := WalkingPair.left }s:Cone (pair emptyIG emptyIG)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s =
s.Ο.app { as := WalkingPair.right }
all_goals
s:Cone (pair emptyIG emptyIG)xβ:Discrete WalkingPairβ’ (β((BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).1 =
(β(s.Ο.app { as := WalkingPair.right })).1s:Cone (pair emptyIG emptyIG)xβ:Discrete WalkingPairβ’ (β((BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).2 =
(β(s.Ο.app { as := WalkingPair.right })).2 s:Cone (pair emptyIG emptyIG)xβ:Discrete WalkingPairβ’ (β((BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).1 =
(β(s.Ο.app { as := WalkingPair.right })).1s:Cone (pair emptyIG emptyIG)xβ:Discrete WalkingPairβ’ (β((BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).2 =
(β(s.Ο.app { as := WalkingPair.right })).2 s:Cone (pair emptyIG emptyIG)xβ:Discrete WalkingPairx:s.pt.carrierDβ’ (β((BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).2 x =
(β(s.Ο.app { as := WalkingPair.right })).2 x
s:Cone (pair emptyIG emptyIG)xβ:Discrete WalkingPairx:s.pt.carrierAβ’ (β((BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).1 x =
(β(s.Ο.app { as := WalkingPair.right })).1 x All goals completed! π
s:Cone (pair emptyIG emptyIG)xβ:Discrete WalkingPairx:s.pt.carrierDβ’ (β((BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).2 x =
(β(s.Ο.app { as := WalkingPair.right })).2 x All goals completed! π
uniq s m _ := s:Cone (pair emptyIG emptyIG)m:s.pt βΆ (BinaryFan.mk (π emptyIG) (π emptyIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app j β m = s.Ο.app jβ’ m = BinaryFan.fst s
s:Cone (pair emptyIG emptyIG)m:s.pt βΆ (BinaryFan.mk (π emptyIG) (π emptyIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app j β m = s.Ο.app jβ’ (βm).1 = (β(BinaryFan.fst s)).1s:Cone (pair emptyIG emptyIG)m:s.pt βΆ (BinaryFan.mk (π emptyIG) (π emptyIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app j β m = s.Ο.app jβ’ (βm).2 = (β(BinaryFan.fst s)).2 s:Cone (pair emptyIG emptyIG)m:s.pt βΆ (BinaryFan.mk (π emptyIG) (π emptyIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app j β m = s.Ο.app jβ’ (βm).1 = (β(BinaryFan.fst s)).1s:Cone (pair emptyIG emptyIG)m:s.pt βΆ (BinaryFan.mk (π emptyIG) (π emptyIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app j β m = s.Ο.app jβ’ (βm).2 = (β(BinaryFan.fst s)).2 s:Cone (pair emptyIG emptyIG)m:s.pt βΆ (BinaryFan.mk (π emptyIG) (π emptyIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app j β m = s.Ο.app jx:s.pt.carrierDβ’ (βm).2 x = (β(BinaryFan.fst s)).2 x
s:Cone (pair emptyIG emptyIG)m:s.pt βΆ (BinaryFan.mk (π emptyIG) (π emptyIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app j β m = s.Ο.app jx:s.pt.carrierAβ’ (βm).1 x = (β(BinaryFan.fst s)).1 x All goals completed! π
s:Cone (pair emptyIG emptyIG)m:s.pt βΆ (BinaryFan.mk (π emptyIG) (π emptyIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π emptyIG) (π emptyIG)).Ο.app j β m = s.Ο.app jx:s.pt.carrierDβ’ (βm).2 x = (β(BinaryFan.fst s)).2 x All goals completed! π
}
-- Naked dot
open IrreflexiveGraph in
example : IsLimit (BinaryFan.mk (π D) (π D)) := β’ IsLimit (BinaryFan.mk (π D) (π D))
exact {
lift s := BinaryFan.fst s
fac s := fun β¨jβ© β¦ s:Cone (pair D D)xβ:Discrete WalkingPairj:WalkingPairβ’ (BinaryFan.mk (π D) (π D)).Ο.app { as := j } β BinaryFan.fst s = s.Ο.app { as := j }
s:Cone (pair D D)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π D) (π D)).Ο.app { as := WalkingPair.left } β BinaryFan.fst s = s.Ο.app { as := WalkingPair.left }s:Cone (pair D D)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π D) (π D)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s = s.Ο.app { as := WalkingPair.right }
all_goals
s:Cone (pair D D)xβ:Discrete WalkingPairβ’ (β((BinaryFan.mk (π D) (π D)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).1 =
(β(s.Ο.app { as := WalkingPair.right })).1s:Cone (pair D D)xβ:Discrete WalkingPairβ’ (β((BinaryFan.mk (π D) (π D)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).2 =
(β(s.Ο.app { as := WalkingPair.right })).2 s:Cone (pair D D)xβ:Discrete WalkingPairβ’ (β((BinaryFan.mk (π D) (π D)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).1 =
(β(s.Ο.app { as := WalkingPair.right })).1s:Cone (pair D D)xβ:Discrete WalkingPairβ’ (β((BinaryFan.mk (π D) (π D)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).2 =
(β(s.Ο.app { as := WalkingPair.right })).2 s:Cone (pair D D)xβ:Discrete WalkingPairx:s.pt.carrierDβ’ (β((BinaryFan.mk (π D) (π D)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).2 x =
(β(s.Ο.app { as := WalkingPair.right })).2 x
s:Cone (pair D D)xβ:Discrete WalkingPairx:s.pt.carrierAβ’ (β((BinaryFan.mk (π D) (π D)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).1 x =
(β(s.Ο.app { as := WalkingPair.right })).1 x All goals completed! π
s:Cone (pair D D)xβ:Discrete WalkingPairx:s.pt.carrierDβ’ (β((BinaryFan.mk (π D) (π D)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).2 x =
(β(s.Ο.app { as := WalkingPair.right })).2 x All goals completed! π
uniq s m _ := s:Cone (pair D D)m:s.pt βΆ (BinaryFan.mk (π D) (π D)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π D) (π D)).Ο.app j β m = s.Ο.app jβ’ m = BinaryFan.fst s
s:Cone (pair D D)m:s.pt βΆ (BinaryFan.mk (π D) (π D)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π D) (π D)).Ο.app j β m = s.Ο.app jβ’ (βm).1 = (β(BinaryFan.fst s)).1s:Cone (pair D D)m:s.pt βΆ (BinaryFan.mk (π D) (π D)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π D) (π D)).Ο.app j β m = s.Ο.app jβ’ (βm).2 = (β(BinaryFan.fst s)).2 s:Cone (pair D D)m:s.pt βΆ (BinaryFan.mk (π D) (π D)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π D) (π D)).Ο.app j β m = s.Ο.app jβ’ (βm).1 = (β(BinaryFan.fst s)).1s:Cone (pair D D)m:s.pt βΆ (BinaryFan.mk (π D) (π D)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π D) (π D)).Ο.app j β m = s.Ο.app jβ’ (βm).2 = (β(BinaryFan.fst s)).2 s:Cone (pair D D)m:s.pt βΆ (BinaryFan.mk (π D) (π D)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π D) (π D)).Ο.app j β m = s.Ο.app jx:s.pt.carrierDβ’ (βm).2 x = (β(BinaryFan.fst s)).2 x
s:Cone (pair D D)m:s.pt βΆ (BinaryFan.mk (π D) (π D)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π D) (π D)).Ο.app j β m = s.Ο.app jx:s.pt.carrierAβ’ (βm).1 x = (β(BinaryFan.fst s)).1 x All goals completed! π
s:Cone (pair D D)m:s.pt βΆ (BinaryFan.mk (π D) (π D)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π D) (π D)).Ο.app j β m = s.Ο.app jx:s.pt.carrierDβ’ (βm).2 x = (β(BinaryFan.fst s)).2 x All goals completed! π
}
-- Single dot with one looping arrow (terminal object in πΊβ)
open IrreflexiveGraph in
example : IsLimit (BinaryFan.mk (π termIG) (π termIG)) := β’ IsLimit (BinaryFan.mk (π termIG) (π termIG))
exact {
lift s := BinaryFan.fst s
fac s := fun β¨jβ© β¦ s:Cone (pair termIG termIG)xβ:Discrete WalkingPairj:WalkingPairβ’ (BinaryFan.mk (π termIG) (π termIG)).Ο.app { as := j } β BinaryFan.fst s = s.Ο.app { as := j }
s:Cone (pair termIG termIG)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π termIG) (π termIG)).Ο.app { as := WalkingPair.left } β BinaryFan.fst s =
s.Ο.app { as := WalkingPair.left }s:Cone (pair termIG termIG)xβ:Discrete WalkingPairβ’ (BinaryFan.mk (π termIG) (π termIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s =
s.Ο.app { as := WalkingPair.right }
all_goals
s:Cone (pair termIG termIG)xβ:Discrete WalkingPairβ’ (β((BinaryFan.mk (π termIG) (π termIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).1 =
(β(s.Ο.app { as := WalkingPair.right })).1s:Cone (pair termIG termIG)xβ:Discrete WalkingPairβ’ (β((BinaryFan.mk (π termIG) (π termIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).2 =
(β(s.Ο.app { as := WalkingPair.right })).2 s:Cone (pair termIG termIG)xβ:Discrete WalkingPairβ’ (β((BinaryFan.mk (π termIG) (π termIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).1 =
(β(s.Ο.app { as := WalkingPair.right })).1s:Cone (pair termIG termIG)xβ:Discrete WalkingPairβ’ (β((BinaryFan.mk (π termIG) (π termIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).2 =
(β(s.Ο.app { as := WalkingPair.right })).2 (s:Cone (pair termIG termIG)xβ:Discrete WalkingPairx:s.pt.carrierDβ’ (β((BinaryFan.mk (π termIG) (π termIG)).Ο.app { as := WalkingPair.right } β BinaryFan.fst s)).2 x =
(β(s.Ο.app { as := WalkingPair.right })).2 x; All goals completed! π)
uniq s m _ := s:Cone (pair termIG termIG)m:s.pt βΆ (BinaryFan.mk (π termIG) (π termIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π termIG) (π termIG)).Ο.app j β m = s.Ο.app jβ’ m = BinaryFan.fst s
s:Cone (pair termIG termIG)m:s.pt βΆ (BinaryFan.mk (π termIG) (π termIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π termIG) (π termIG)).Ο.app j β m = s.Ο.app jβ’ (βm).1 = (β(BinaryFan.fst s)).1s:Cone (pair termIG termIG)m:s.pt βΆ (BinaryFan.mk (π termIG) (π termIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π termIG) (π termIG)).Ο.app j β m = s.Ο.app jβ’ (βm).2 = (β(BinaryFan.fst s)).2 s:Cone (pair termIG termIG)m:s.pt βΆ (BinaryFan.mk (π termIG) (π termIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π termIG) (π termIG)).Ο.app j β m = s.Ο.app jβ’ (βm).1 = (β(BinaryFan.fst s)).1s:Cone (pair termIG termIG)m:s.pt βΆ (BinaryFan.mk (π termIG) (π termIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π termIG) (π termIG)).Ο.app j β m = s.Ο.app jβ’ (βm).2 = (β(BinaryFan.fst s)).2 (s:Cone (pair termIG termIG)m:s.pt βΆ (BinaryFan.mk (π termIG) (π termIG)).ptxβ:β (j : Discrete WalkingPair), (BinaryFan.mk (π termIG) (π termIG)).Ο.app j β m = s.Ο.app jx:s.pt.carrierDβ’ (βm).2 x = (β(BinaryFan.fst s)).2 x; All goals completed! π)
}
Exercise 4 (p. 292)
The inverse, call it g, of the isomorphism of sets {\mathbb{N} \xrightarrow{f} \mathbb{N} \times \mathbb{N}} above [the Cantor pairing function] is actually given by a quadratic polynomial, of the form
g(x, y) = \tfrac{1}{2}(ax^2 + bxy + cy^2 + dx + ey)
where a, b, c, d, and e are fixed natural numbers. Can you find them? Can you prove that the map g defined by your formula is an isomorphism of sets? You might expect that f would have a simpler formula than its inverse g, since a map {\mathbb{N} \xrightarrow{f} \mathbb{N} \times \mathbb{N}} amounts to a pair of maps {f_1 = p_1 f} and {f_2 = p_2 f} from \mathbb{N} to \mathbb{N}. But f_1 and f_2 are not so simple. In fact, no matter what isomorphism {\mathbb{N} \xrightarrow{f} \mathbb{N} \times \mathbb{N}} you choose, f_1 cannot be given by a polynomial. Can you see why?
Solution: Exercise 4
Let the pair {(x, y)} be an arbitary element of {\mathbb{N} \times \mathbb{N}}, and let {n = x + y}. Then the total number of pairs in all northwest diagonals strictly preceding the n-th diagonal is the n-th triangular number {T_n = \frac{1}{2}n(n + 1)}. To obtain the exact position of the pair {(x, y)} on the n-th diagonal, we add y to T_n. Thus, the formula for g is
g(x, y) = \tfrac{1}{2}(x + y)(x + y + 1) + y = \tfrac{1}{2}(x^2 + 2xy + y^2 + x + 3y).
To prove that g is an isomorphism of sets, we show that g is a bijective function. (We apply the grind tactic liberally in the remaining proofs in this exercise to keep them succinct.)
We begin our proof by defining triangular numbers and the function g.
def tri : β β β
| 0 => 0
| n + 1 => tri n + n + 1
def g : β Γ β βΆ β := fun (x, y) β¦ tri (x + y) + y
Next we define some helper lemmas.
lemma tri_le_of_le {a b : β} (h : a β€ b) : tri a β€ tri b := a:βb:βh:a β€ bβ’ tri a β€ tri b
a:βb:ββ’ tri a β€ tri aa:βb:βmβ:βaβ:a.le mβa_ihβ:tri a β€ tri mββ’ tri a β€ tri mβ.succ
case refl a:βb:ββ’ tri a β€ tri a All goals completed! π
case step m _ ih a:βb:βm:βaβ:a.le mβih:tri a β€ tri mββ’ tri a β€ tri mβ.succ
All goals completed! π
lemma g_ubound {x y : β} : g (x, y) < tri (x + y + 1) := x:βy:ββ’ g (x, y) < tri (x + y + 1)
All goals completed! π
lemma g_lbound {x y : β} : tri (x + y) β€ g (x, y) :=
Nat.le_add_right (tri (x + y)) y
lemma eq_of_g_eq {x y x' y' : β} (h : g (x, y) = g (x', y')) :
x + y = x' + y' := x:βy:βx':βy':βh:g (x, y) = g (x', y')β’ x + y = x' + y'
x:βy:βx':βy':βh:g (x, y) = g (x', y')hlt:x + y < x' + y'β’ x + y = x' + y'x:βy:βx':βy':βh:g (x, y) = g (x', y')heq:x + y = x' + y'β’ x + y = x' + y'x:βy:βx':βy':βh:g (x, y) = g (x', y')hgt:x' + y' < x + yβ’ x + y = x' + y'
x:βy:βx':βy':βh:g (x, y) = g (x', y')hlt:x + y < x' + y'β’ x + y = x' + y' All goals completed! π
x:βy:βx':βy':βh:g (x, y) = g (x', y')heq:x + y = x' + y'β’ x + y = x' + y' All goals completed! π
x:βy:βx':βy':βh:g (x, y) = g (x', y')hgt:x' + y' < x + yβ’ x + y = x' + y' All goals completed! π
lemma exists_tri_bound (z : β) :
β n : β, tri n β€ z β§ z < tri (n + 1) := z:ββ’ β n, tri n β€ z β§ z < tri (n + 1)
induction z with
β’ β n, tri n β€ 0 β§ 0 < tri (n + 1) All goals completed! π
z:βih:β n, tri n β€ z β§ z < tri (n + 1)β’ β n, tri n β€ z + 1 β§ z + 1 < tri (n + 1) All goals completed! π
Finally we prove that g is an isomorphism of sets.
example : IsIso g := β’ IsIso g
β’ Function.Bijective g
β’ Function.Injective gβ’ Function.Surjective g
β’ Function.Injective g β’ Function.Injective g
intro β¨x, yβ© x:βy:βx':βy':ββ’ g (x, y) = g (x', y') β (x, y) = (x', y') x:βy:βx':βy':βh:g (x, y) = g (x', y')β’ (x, y) = (x', y')
All goals completed! π
β’ Function.Surjective g β’ Function.Surjective g
z:ββ’ β a, g a = z
z:βw:βleftβ:tri w β€ zrightβ:z < tri (w + 1)β’ β a, g a = z
z:βw:βleftβ:tri w β€ zrightβ:z < tri (w + 1)β’ g (w - (z - tri w), z - tri w) = z
All goals completed! π
The final part of the exercise asks us to show that no isomorphism {\mathbb{N} \xrightarrow{f} \mathbb{N} \times \mathbb{N}} can have a polynomial as its first component function f_1.
In the proof below, we assume that such a polynomial P exists and derive a contradiction. Since f is an isomorphism and hence bijective, it maps infinitely many inputs to pairs starting with any given integer k. Therefore P must also evaluate to k infinitely many times. However, a non-constant polynomial can only have a finite number of roots, meaning P must be the constant polynomial {P(x) = k} for any k. Hence P is forced to be simultaneously the constant polynomial 0 and the constant polynomial 1, yielding the impossible result that {0 = 1}.
open Polynomial in
example (f : β βΆ β Γ β) [IsIso f] :
Β¬β P : β€[X], β n : β, P.eval (n : β€) = (f n).1 := f:β βΆ β Γ βinstβ:IsIso fβ’ Β¬β P, β (n : β), Polynomial.eval (βn) P = β(f n).1
-- Convert isomorphism f to equivalence f'
f:β βΆ β Γ βinstβ:IsIso ff':β β β Γ β := (asIso f).toEquivβ’ Β¬β P, β (n : β), Polynomial.eval (βn) P = β(f n).1
-- Provide translation for grind
f:β βΆ β Γ βinstβ:IsIso ff':β β β Γ β := (asIso f).toEquivthis:β (n : β), f n = f' nβ’ Β¬β P, β (n : β), Polynomial.eval (βn) P = β(f n).1
f:β βΆ β Γ βinstβ:IsIso ff':β β β Γ β := (asIso f).toEquivthis:β (n : β), f n = f' nP:β€[X]hP:β (n : β), Polynomial.eval (βn) P = β(f n).1β’ False
-- Show polynomial P must equal constant polynomial C k for any k
have h_P_eq_C (k : β) : P = C (k : β€) := f:β βΆ β Γ βinstβ:IsIso fβ’ Β¬β P, β (n : β), Polynomial.eval (βn) P = β(f n).1
-- Equate preimage of set {k} Γ β to roots of P = k
have h_eq : f' β»ΒΉ' {p : β Γ β | (p.1 : β€) = k} =
{n : β | P.eval (n : β€) = k} := f:β βΆ β Γ βinstβ:IsIso fβ’ Β¬β P, β (n : β), Polynomial.eval (βn) P = β(f n).1
All goals completed! π
-- Register type class 'Infinite' for set {k} Γ β
have : Infinite {p : β Γ β | (p.1 : β€) = k} := f:β βΆ β Γ βinstβ:IsIso fβ’ Β¬β P, β (n : β), Polynomial.eval (βn) P = β(f n).1
f:β βΆ β Γ βinstβ:IsIso ff':β β β Γ β := (asIso f).toEquivthis:β (n : β), f n = f' nP:β€[X]hP:β (n : β), Polynomial.eval (βn) P = β(f n).1k:βh_eq:βf' β»ΒΉ' {p | βp.1 = βk} = {n | Polynomial.eval (βn) P = βk}β’ Function.Injective fun n β¦ β¨(k, n), β―β©
All goals completed! π
-- Prove there are infinitely many inputs where P evaluates to k
have h_infinite : Infinite {n : β | P.eval (n : β€) = k} := f:β βΆ β Γ βinstβ:IsIso fβ’ Β¬β P, β (n : β), Polynomial.eval (βn) P = β(f n).1
f:β βΆ β Γ βinstβ:IsIso ff':β β β Γ β := (asIso f).toEquivthisβ:β (n : β), f n = f' nP:β€[X]hP:β (n : β), Polynomial.eval (βn) P = β(f n).1k:βh_eq:βf' β»ΒΉ' {p | βp.1 = βk} = {n | Polynomial.eval (βn) P = βk}this:Infinite β{p | βp.1 = βk}β’ Infinite β(βf' β»ΒΉ' {p | βp.1 = βk})
apply Infinite.of_injective
(fun s : {p : β Γ β | (p.1 : β€) = k} β¦
β¨f'.symm s.val, f:β βΆ β Γ βinstβ:IsIso ff':β β β Γ β := (asIso f).toEquivthisβ:β (n : β), f n = f' nP:β€[X]hP:β (n : β), Polynomial.eval (βn) P = β(f n).1k:βh_eq:βf' β»ΒΉ' {p | βp.1 = βk} = {n | Polynomial.eval (βn) P = βk}this:Infinite β{p | βp.1 = βk}s:β{p | βp.1 = βk}β’ f'.symm βs β βf' β»ΒΉ' {p | βp.1 = βk} All goals completed! πβ©)
All goals completed! π
-- Assume towards a contradiction that P does not equal C k
f:β βΆ β Γ βinstβ:IsIso ff':β β β Γ β := (asIso f).toEquivthisβ:β (n : β), f n = f' nP:β€[X]hP:β (n : β), Polynomial.eval (βn) P = β(f n).1k:βh_eq:βf' β»ΒΉ' {p | βp.1 = βk} = {n | Polynomial.eval (βn) P = βk}this:Infinite β{p | βp.1 = βk}h_infinite:Infinite β{n | Polynomial.eval (βn) P = βk}hc:Β¬P = C βkβ’ False
-- Map infinite inputs injectively to finite roots of P = k
let toRoots : {n : β | P.eval (n : β€) = k} β
(P - C (k : β€)).roots.toFinset := fun z β¦
β¨z.val, f:β βΆ β Γ βinstβ:IsIso ff':β β β Γ β := (asIso f).toEquivthisβ:β (n : β), f n = f' nP:β€[X]hP:β (n : β), Polynomial.eval (βn) P = β(f n).1k:βh_eq:βf' β»ΒΉ' {p | βp.1 = βk} = {n | Polynomial.eval (βn) P = βk}this:Infinite β{p | βp.1 = βk}h_infinite:Infinite β{n | Polynomial.eval (βn) P = βk}hc:Β¬P = C βkz:β{n | Polynomial.eval (βn) P = βk}β’ ββz β (P - C βk).roots.toFinset All goals completed! πβ©
-- Set up contradiction by showing our set is finite
have h_fin : Finite {n : β | P.eval (n : β€) = k} :=
Finite.of_injective toRoots (f:β βΆ β Γ βinstβ:IsIso ff':β β β Γ β := (asIso f).toEquivthisβ:β (n : β), f n = f' nP:β€[X]hP:β (n : β), Polynomial.eval (βn) P = β(f n).1k:βh_eq:βf' β»ΒΉ' {p | βp.1 = βk} = {n | Polynomial.eval (βn) P = βk}this:Infinite β{p | βp.1 = βk}h_infinite:Infinite β{n | Polynomial.eval (βn) P = βk}hc:Β¬P = C βktoRoots:β{n | Polynomial.eval (βn) P = βk} β β₯(P - C βk).roots.toFinset := fun z β¦ β¨ββz, β―β©β’ Function.Injective toRoots All goals completed! π)
-- and also not finite
f:β βΆ β Γ βinstβ:IsIso ff':β β β Γ β := (asIso f).toEquivthisβ:β (n : β), f n = f' nP:β€[X]hP:β (n : β), Polynomial.eval (βn) P = β(f n).1k:βh_eq:βf' β»ΒΉ' {p | βp.1 = βk} = {n | Polynomial.eval (βn) P = βk}this:Infinite β{p | βp.1 = βk}h_infinite:Infinite β{n | Polynomial.eval (βn) P = βk}hc:Β¬P = C βktoRoots:β{n | Polynomial.eval (βn) P = βk} β β₯(P - C βk).roots.toFinset := fun z β¦ β¨ββz, β―β©h_fin:Finite β{n | Polynomial.eval (βn) P = βk}h_not_fin:Β¬Finite β{n | Polynomial.eval (βn) P = βk}β’ False
All goals completed! π
-- Conclude P must equal both 0 and 1, forcing 0 = 1
f:β βΆ β Γ βinstβ:IsIso ff':β β β Γ β := (asIso f).toEquivthis:β (n : β), f n = f' nP:β€[X]hP:β (n : β), Polynomial.eval (βn) P = β(f n).1h_P_eq_C:β (k : β), P = C βkhC:C 0 = C 1β’ False
All goals completed! π
4. Solving equations and picturing maps
Definition: Equalizer (p. 292)
{E \xrightarrow{p} X} is an equalizer of {f, g} if {fp = gp} and for each {T \xrightarrow{x} X} for which {fx = gx}, there is exactly one {T \xrightarrow{e} E} for which {x = pe}.
In mathlib, two parallel morphisms f and g are given by the diagram parallelPair f g. A cone over parallelPair f g is aliased as Fork f g. If that fork is a limit cone, then we have an equalizer of {f, g}. We print the definitions of HasEqualizer, parallelPair, and Fork below for reference.
#print HasEqualizer
#check parallelPair
#print Fork
Exercise 5 (p. 293)
If both {E, p} and {F, q} are equalizers for the same pair {f, g}, then the unique map {F \xrightarrow{e} E} for which {pe = q} is an isomorphism.
Solution: Exercise 5
Using Mathlib's canonical equalizer f g function would make both {E, p} and {F, q} into the exact same chosen object, reducing the exercise to a triviality about the identity morphism. To preserve the purpose of the exercise, which is to compare two independent equalizers, our proof uses the book definition directly.
example {π : Type u} [Category.{v, u} π]
(X Y : π) (f g : X βΆ Y) (E F : π)
(p : E βΆ X) (hpβ : f β p = g β p)
(hpβ : β (T : π) (x : T βΆ X), f β x = g β x β
β! e : T βΆ E, x = p β e)
(q : F βΆ X) (hqβ : f β q = g β q)
(hqβ : β (T : π) (x : T βΆ X), f β x = g β x β
β! e : T βΆ F, x = q β e) :
β e : F β
E, p β e.hom = q := π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πF:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eq:F βΆ Xhqβ:f β q = g β qhqβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = q β eβ’ β e, p β e.hom = q
π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πF:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eq:F βΆ Xhqβ:f β q = g β qhqβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = q β ee:F βΆ Ehe_comm:q = p β erightβ:β (y : F βΆ E), (fun e β¦ q = p β e) y β y = eβ’ β e, p β e.hom = q
π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πF:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eq:F βΆ Xhqβ:f β q = g β qhqβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = q β ee:F βΆ Ehe_comm:q = p β erightβΒΉ:β (y : F βΆ E), (fun e β¦ q = p β e) y β y = ee_inv:E βΆ Fhe_inv_comm:p = q β e_invrightβ:β (y : E βΆ F), (fun e β¦ p = q β e) y β y = e_invβ’ β e, p β e.hom = q
π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πF:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eq:F βΆ Xhqβ:f β q = g β qhqβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = q β ee:F βΆ Ehe_comm:q = p β erightβΒΉ:β (y : F βΆ E), (fun e β¦ q = p β e) y β y = ee_inv:E βΆ Fhe_inv_comm:p = q β e_invrightβ:β (y : E βΆ F), (fun e β¦ p = q β e) y β y = e_invwβ:E βΆ Eleftβ:p = p β wβhE_uniq:β (y : E βΆ E), (fun e β¦ p = p β e) y β y = wββ’ β e, p β e.hom = q
π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πF:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eq:F βΆ Xhqβ:f β q = g β qhqβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = q β ee:F βΆ Ehe_comm:q = p β erightβΒΉ:β (y : F βΆ E), (fun e β¦ q = p β e) y β y = ee_inv:E βΆ Fhe_inv_comm:p = q β e_invrightβ:β (y : E βΆ F), (fun e β¦ p = q β e) y β y = e_invwβ:E βΆ Eleftβ:p = p β wβhE_uniq:β (y : E βΆ E), (fun e β¦ p = p β e) y β y = wβhEβ:π E = wββ’ β e, p β e.hom = q
have hEβ := hE_uniq (e β e_inv)
(π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πF:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eq:F βΆ Xhqβ:f β q = g β qhqβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = q β ee:F βΆ Ehe_comm:q = p β erightβΒΉ:β (y : F βΆ E), (fun e β¦ q = p β e) y β y = ee_inv:E βΆ Fhe_inv_comm:p = q β e_invrightβ:β (y : E βΆ F), (fun e β¦ p = q β e) y β y = e_invwβ:E βΆ Eleftβ:p = p β wβhE_uniq:β (y : E βΆ E), (fun e β¦ p = p β e) y β y = wβhEβ:π E = wββ’ (fun e β¦ p = p β e) (e β e_inv) π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πF:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eq:F βΆ Xhqβ:f β q = g β qhqβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = q β ee:F βΆ Ehe_comm:q = p β erightβΒΉ:β (y : F βΆ E), (fun e β¦ q = p β e) y β y = ee_inv:E βΆ Fhe_inv_comm:p = q β e_invrightβ:β (y : E βΆ F), (fun e β¦ p = q β e) y β y = e_invwβ:E βΆ Eleftβ:p = p β wβhE_uniq:β (y : E βΆ E), (fun e β¦ p = p β e) y β y = wβhEβ:π E = wββ’ p = p β e β e_inv; All goals completed! π)
π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πF:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eq:F βΆ Xhqβ:f β q = g β qhqβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = q β ee:F βΆ Ehe_comm:q = p β erightβΒΉ:β (y : F βΆ E), (fun e β¦ q = p β e) y β y = ee_inv:E βΆ Fhe_inv_comm:p = q β e_invrightβ:β (y : E βΆ F), (fun e β¦ p = q β e) y β y = e_invwβΒΉ:E βΆ EleftβΒΉ:p = p β wβhE_uniq:β (y : E βΆ E), (fun e β¦ p = p β e) y β y = wβhEβ:π E = wβhEβ:e β e_inv = wβΒΉwβ:F βΆ Fleftβ:q = q β wβhF_uniq:β (y : F βΆ F), (fun e β¦ q = q β e) y β y = wββ’ β e, p β e.hom = q
π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πF:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eq:F βΆ Xhqβ:f β q = g β qhqβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = q β ee:F βΆ Ehe_comm:q = p β erightβΒΉ:β (y : F βΆ E), (fun e β¦ q = p β e) y β y = ee_inv:E βΆ Fhe_inv_comm:p = q β e_invrightβ:β (y : E βΆ F), (fun e β¦ p = q β e) y β y = e_invwβΒΉ:E βΆ EleftβΒΉ:p = p β wβhE_uniq:β (y : E βΆ E), (fun e β¦ p = p β e) y β y = wβhEβ:π E = wβhEβ:e β e_inv = wβΒΉwβ:F βΆ Fleftβ:q = q β wβhF_uniq:β (y : F βΆ F), (fun e β¦ q = q β e) y β y = wβhFβ:π F = wββ’ β e, p β e.hom = q
have hFβ := hF_uniq (e_inv β e)
(π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πF:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eq:F βΆ Xhqβ:f β q = g β qhqβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = q β ee:F βΆ Ehe_comm:q = p β erightβΒΉ:β (y : F βΆ E), (fun e β¦ q = p β e) y β y = ee_inv:E βΆ Fhe_inv_comm:p = q β e_invrightβ:β (y : E βΆ F), (fun e β¦ p = q β e) y β y = e_invwβΒΉ:E βΆ EleftβΒΉ:p = p β wβhE_uniq:β (y : E βΆ E), (fun e β¦ p = p β e) y β y = wβhEβ:π E = wβhEβ:e β e_inv = wβΒΉwβ:F βΆ Fleftβ:q = q β wβhF_uniq:β (y : F βΆ F), (fun e β¦ q = q β e) y β y = wβhFβ:π F = wββ’ (fun e β¦ q = q β e) (e_inv β e) π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πF:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eq:F βΆ Xhqβ:f β q = g β qhqβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = q β ee:F βΆ Ehe_comm:q = p β erightβΒΉ:β (y : F βΆ E), (fun e β¦ q = p β e) y β y = ee_inv:E βΆ Fhe_inv_comm:p = q β e_invrightβ:β (y : E βΆ F), (fun e β¦ p = q β e) y β y = e_invwβΒΉ:E βΆ EleftβΒΉ:p = p β wβhE_uniq:β (y : E βΆ E), (fun e β¦ p = p β e) y β y = wβhEβ:π E = wβhEβ:e β e_inv = wβΒΉwβ:F βΆ Fleftβ:q = q β wβhF_uniq:β (y : F βΆ F), (fun e β¦ q = q β e) y β y = wβhFβ:π F = wββ’ q = q β e_inv β e; All goals completed! π)
use {
hom := e
inv := e_inv
hom_inv_id := π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πF:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eq:F βΆ Xhqβ:f β q = g β qhqβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = q β ee:F βΆ Ehe_comm:q = p β erightβΒΉ:β (y : F βΆ E), (fun e β¦ q = p β e) y β y = ee_inv:E βΆ Fhe_inv_comm:p = q β e_invrightβ:β (y : E βΆ F), (fun e β¦ p = q β e) y β y = e_invwβΒΉ:E βΆ EleftβΒΉ:p = p β wβhE_uniq:β (y : E βΆ E), (fun e β¦ p = p β e) y β y = wβhEβ:π E = wβhEβ:e β e_inv = wβΒΉwβ:F βΆ Fleftβ:q = q β wβhF_uniq:β (y : F βΆ F), (fun e β¦ q = q β e) y β y = wβhFβ:π F = wβhFβ:e_inv β e = wββ’ e_inv β e = π F All goals completed! π
inv_hom_id := π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πF:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eq:F βΆ Xhqβ:f β q = g β qhqβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = q β ee:F βΆ Ehe_comm:q = p β erightβΒΉ:β (y : F βΆ E), (fun e β¦ q = p β e) y β y = ee_inv:E βΆ Fhe_inv_comm:p = q β e_invrightβ:β (y : E βΆ F), (fun e β¦ p = q β e) y β y = e_invwβΒΉ:E βΆ EleftβΒΉ:p = p β wβhE_uniq:β (y : E βΆ E), (fun e β¦ p = p β e) y β y = wβhEβ:π E = wβhEβ:e β e_inv = wβΒΉwβ:F βΆ Fleftβ:q = q β wβhF_uniq:β (y : F βΆ F), (fun e β¦ q = q β e) y β y = wβhFβ:π F = wβhFβ:e_inv β e = wββ’ e β e_inv = π E All goals completed! π
}
All goals completed! π
Exercise 6 (p. 293)
Any map p which is an equalizer of some pair of maps is itself a monomorphism (i.e. injective).
Solution: Exercise 6
Using the book definition of equalizer, we have
example {π : Type u} [Category.{v, u} π]
(X Y : π) (f g : X βΆ Y) (E : π)
(p : E βΆ X) (hpβ : f β p = g β p)
(hpβ : β (T : π) (x : T βΆ X), f β x = g β x β
β! e : T βΆ E, x = p β e) :
Mono p := π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eβ’ Mono p
π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eβ’ β {Z : π} (g h : Z βΆ E), p β g = p β h β g = h
intro T π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eT:πeβ:T βΆ Eβ’ β (h : T βΆ E), p β eβ = p β h β eβ = h π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eT:πeβ:T βΆ Eeβ:T βΆ Eβ’ p β eβ = p β eβ β eβ = eβ π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eT:πeβ:T βΆ Eeβ:T βΆ Eh_eqβ:p β eβ = p β eββ’ eβ = eβ
have h_eqβ : f β p β eβ = g β p β eβ := π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eβ’ Mono p
All goals completed! π
π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YE:πp:E βΆ Xhpβ:f β p = g β phpβ:β (T : π) (x : T βΆ X), f β x = g β x β β! e, x = p β eT:πeβ:T βΆ Eeβ:T βΆ Eh_eqβ:p β eβ = p β eβh_eqβ:f β p β eβ = g β p β eβwβ:T βΆ Eleftβ:p β eβ = p β wβh_uniq:β (y : T βΆ E), (fun e β¦ p β eβ = p β e) y β y = wββ’ eβ = eβ
All goals completed! π
Alternatively, using mathlib's HasEqualizer type class and the equalizer.hom_ext theorem yields a more concise proof.
example {π : Type u} [Category.{v, u} π]
(X Y : π) (f g : X βΆ Y) [HasEqualizer f g] :
Mono (equalizer.ΞΉ f g) := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasEqualizer f gβ’ Mono (equalizer.ΞΉ f g)
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasEqualizer f gp:equalizer f g βΆ X := equalizer.ΞΉ f gβ’ Mono (equalizer.ΞΉ f g)
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasEqualizer f gp:equalizer f g βΆ X := equalizer.ΞΉ f gβ’ β {Z : π} (g_1 h : Z βΆ equalizer f g), equalizer.ΞΉ f g β g_1 = equalizer.ΞΉ f g β h β g_1 = h
intro T π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasEqualizer f gp:equalizer f g βΆ X := equalizer.ΞΉ f gT:πeβ:T βΆ equalizer f gβ’ β (h : T βΆ equalizer f g), equalizer.ΞΉ f g β eβ = equalizer.ΞΉ f g β h β eβ = h π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasEqualizer f gp:equalizer f g βΆ X := equalizer.ΞΉ f gT:πeβ:T βΆ equalizer f geβ:T βΆ equalizer f gβ’ equalizer.ΞΉ f g β eβ = equalizer.ΞΉ f g β eβ β eβ = eβ π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasEqualizer f gp:equalizer f g βΆ X := equalizer.ΞΉ f gT:πeβ:T βΆ equalizer f geβ:T βΆ equalizer f gh_eq:equalizer.ΞΉ f g β eβ = equalizer.ΞΉ f g β eββ’ eβ = eβ
All goals completed! π
Exercise 7 (p. 293)
If {B \xrightarrow{\alpha} A \xrightarrow{\beta} B} compose to the identity {1_B = \beta\alpha} and if f is the idempotent \alpha\beta, then \alpha is an equalizer for the pair {f, 1_A}.
Solution: Exercise 7
Using the book definition of equalizer, we have
example {π : Type u} [Category.{v, u} π]
(A B : π) (Ξ± : B βΆ A) (Ξ² : A βΆ B)
(h_idB : π B = Ξ² β Ξ±) (f : A βΆ A) (hf : f = Ξ± β Ξ²) :
f β Ξ± = π A β Ξ± β§
β (T : π) (x : T βΆ A), f β x = π A β x β
β! e : T βΆ B, x = Ξ± β e := π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²β’ f β Ξ± = π A β Ξ± β§ β (T : π) (x : T βΆ A), f β x = π A β x β β! e, x = Ξ± β e
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²β’ f β Ξ± = π A β Ξ±π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²β’ β (T : π) (x : T βΆ A), f β x = π A β x β β! e, x = Ξ± β e
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²β’ f β Ξ± = π A β Ξ± All goals completed! π
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²β’ β (T : π) (x : T βΆ A), f β x = π A β x β β! e, x = Ξ± β e intro T π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²T:πx:T βΆ Aβ’ f β x = π A β x β β! e, x = Ξ± β e π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²T:πx:T βΆ Ahx:f β x = π A β xβ’ β! e, x = Ξ± β e
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²T:πx:T βΆ Ahx:f β x = π A β xβ’ (fun e β¦ x = Ξ± β e) (Ξ² β x) β§ β (y : T βΆ B), (fun e β¦ x = Ξ± β e) y β y = Ξ² β x
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²T:πx:T βΆ Ahx:f β x = π A β xβ’ (fun e β¦ x = Ξ± β e) (Ξ² β x)π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²T:πx:T βΆ Ahx:f β x = π A β xβ’ β (y : T βΆ B), (fun e β¦ x = Ξ± β e) y β y = Ξ² β x
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²T:πx:T βΆ Ahx:f β x = π A β xβ’ (fun e β¦ x = Ξ± β e) (Ξ² β x) π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²T:πx:T βΆ Ahx:f β x = π A β xβ’ x = Ξ± β Ξ² β x
All goals completed! π
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²T:πx:T βΆ Ahx:f β x = π A β xβ’ β (y : T βΆ B), (fun e β¦ x = Ξ± β e) y β y = Ξ² β x intro y π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²T:πx:T βΆ Ahx:f β x = π A β xy:T βΆ Bhy:x = Ξ± β yβ’ y = Ξ² β x
All goals completed! π
Using the mathlib API, we have
example {π : Type u} [Category.{v, u} π]
(A B : π) (Ξ± : B βΆ A) (Ξ² : A βΆ B)
(h_idB : π B = Ξ² β Ξ±) (f : A βΆ A) (hf : f = Ξ± β Ξ²) :
β (w : f β Ξ± = π A β Ξ±),
Nonempty (IsLimit (Fork.ofΞΉ Ξ± w)) := π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²β’ β (w : f β Ξ± = π A β Ξ±), Nonempty (IsLimit (Fork.ofΞΉ Ξ± w))
have w : f β Ξ± = π A β Ξ± := π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²β’ β (w : f β Ξ± = π A β Ξ±), Nonempty (IsLimit (Fork.ofΞΉ Ξ± w))
All goals completed! π
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²w:f β Ξ± = π A β Ξ±β’ Nonempty (IsLimit (Fork.ofΞΉ Ξ± w))
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²w:f β Ξ± = π A β Ξ±β’ IsLimit (Fork.ofΞΉ Ξ± w)
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²w:f β Ξ± = π A β Ξ±β’ β (s : Fork f (π A)), (Fork.ofΞΉ Ξ± w).ΞΉ β (fun s β¦ Ξ² β s.ΞΉ) s = s.ΞΉπ:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²w:f β Ξ± = π A β Ξ±β’ β (s : Fork f (π A)) (m : s.pt βΆ (Fork.ofΞΉ Ξ± w).pt), (Fork.ofΞΉ Ξ± w).ΞΉ β m = s.ΞΉ β m = (fun s β¦ Ξ² β s.ΞΉ) s
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²w:f β Ξ± = π A β Ξ±β’ β (s : Fork f (π A)), (Fork.ofΞΉ Ξ± w).ΞΉ β (fun s β¦ Ξ² β s.ΞΉ) s = s.ΞΉ -- fac
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²w:f β Ξ± = π A β Ξ±s:Fork f (π A)β’ (Fork.ofΞΉ Ξ± w).ΞΉ β (fun s β¦ Ξ² β s.ΞΉ) s = s.ΞΉ
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²w:f β Ξ± = π A β Ξ±s:Fork f (π A)β’ Ξ± β Ξ² β s.ΞΉ = s.ΞΉ
All goals completed! π
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²w:f β Ξ± = π A β Ξ±β’ β (s : Fork f (π A)) (m : s.pt βΆ (Fork.ofΞΉ Ξ± w).pt), (Fork.ofΞΉ Ξ± w).ΞΉ β m = s.ΞΉ β m = (fun s β¦ Ξ² β s.ΞΉ) s -- uniq
intro s π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²w:f β Ξ± = π A β Ξ±s:Fork f (π A)m:s.pt βΆ (Fork.ofΞΉ Ξ± w).ptβ’ (Fork.ofΞΉ Ξ± w).ΞΉ β m = s.ΞΉ β m = (fun s β¦ Ξ² β s.ΞΉ) s π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²w:f β Ξ± = π A β Ξ±s:Fork f (π A)m:s.pt βΆ (Fork.ofΞΉ Ξ± w).pthm:(Fork.ofΞΉ Ξ± w).ΞΉ β m = s.ΞΉβ’ m = (fun s β¦ Ξ² β s.ΞΉ) s
π:Type uinstβ:Category.{v, u} πA:πB:πΞ±:B βΆ AΞ²:A βΆ Bh_idB:π B = Ξ² β Ξ±f:A βΆ Ahf:f = Ξ± β Ξ²w:f β Ξ± = π A β Ξ±s:Fork f (π A)m:s.pt βΆ (Fork.ofΞΉ Ξ± w).pthm:(Fork.ofΞΉ Ξ± w).ΞΉ β m = s.ΞΉβ’ m = Ξ² β s.ΞΉ
erw [β hm, Category.assoc, β h_idB, Category.comp_idAll goals completed! π
Exercise 8 (p. 293)
Any parallel pair {X \xrightarrow{f} Y}, {X \xrightarrow{g} Y} of maps in sets, no matter how or why it occurred to us in the first place, can always be imagined as the source and target structure of a graph. In a graph, which are the arrows that are named by the equalizer of the source and target maps?
Solution: Exercise 8
In this analogy, the set X represents the arrows of the graph, and the set Y represents the dots. The functions f and g represent the source and target maps. The equalizer of {f, g} is then the subset of elements {x \in X} such that {f(x) = g(x)}, which corresponds to the arrows whose source and target are the same dot. Therefore the arrows named by the equalizer are exactly the self-loops of the graph.
We formalise the proof of this statement below. Instead of using a subset, however, we represent the equalizer as a type E and a morphism p from E to the arrows of the graph, and we assume that p equalizes the source and target maps and satisfies the universal property of a limit.
example (G : IrreflexiveGraph) (E : Type) (p : E βΆ G.carrierA)
(w : G.toSrc β p = G.toTgt β p)
(t : IsLimit (Fork.ofΞΉ p w)) :
β a : G.carrierA, (β x : E, p x = a) β
G.toSrc a = G.toTgt a := G:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)β’ β (a : G.carrierA), (β x, p x = a) β G.toSrc a = G.toTgt a
G:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)a:G.carrierAβ’ (β x, p x = a) β G.toSrc a = G.toTgt a
G:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)a:G.carrierAβ’ (β x, p x = a) β G.toSrc a = G.toTgt aG:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)a:G.carrierAβ’ G.toSrc a = G.toTgt a β β x, p x = a
G:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)a:G.carrierAβ’ (β x, p x = a) β G.toSrc a = G.toTgt a G:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)x:Eβ’ G.toSrc (p x) = G.toTgt (p x)
All goals completed! π
G:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)a:G.carrierAβ’ G.toSrc a = G.toTgt a β β x, p x = a G:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)a:G.carrierAha:G.toSrc a = G.toTgt aβ’ β x, p x = a
-- Convert a : G.carrierA into a morphism from the terminal object
G:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)a:G.carrierAha:G.toSrc a = G.toTgt atest:Unit βΆ G.carrierA := fun x β¦ aβ’ β x, p x = a
-- and show that the morphism equalizes the source and target maps
have h_test : G.toSrc β test = G.toTgt β test := G:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)β’ β (a : G.carrierA), (β x, p x = a) β G.toSrc a = G.toTgt a
G:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)a:G.carrierAha:G.toSrc a = G.toTgt atest:Unit βΆ G.carrierA := fun x β¦ axβ:Unitβ’ (G.toSrc β test) xβ = (G.toTgt β test) xβ
All goals completed! π
-- Bundle the morphism into a cone over the parallel pair of maps
G:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)a:G.carrierAha:G.toSrc a = G.toTgt atest:Unit βΆ G.carrierA := fun x β¦ ah_test:G.toSrc β test = G.toTgt β tests:Fork G.toSrc G.toTgt := Fork.ofΞΉ test h_testβ’ β x, p x = a
-- Use the universal property of the limit to get a witness x : E
G:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)a:G.carrierAha:G.toSrc a = G.toTgt atest:Unit βΆ G.carrierA := fun x β¦ ah_test:G.toSrc β test = G.toTgt β tests:Fork G.toSrc G.toTgt := Fork.ofΞΉ test h_testβ’ p (t.lift s ()) = a
-- Appeal to the factorisation property of the limit
G:IrreflexiveGraphE:Typep:E βΆ G.carrierAw:G.toSrc β p = G.toTgt β pt:IsLimit (Fork.ofΞΉ p w)a:G.carrierAha:G.toSrc a = G.toTgt atest:Unit βΆ G.carrierA := fun x β¦ ah_test:G.toSrc β test = G.toTgt β tests:Fork G.toSrc G.toTgt := Fork.ofΞΉ test h_testh_fac:p β t.lift s = s.ΞΉβ’ p (t.lift s ()) = a
-- Close the goal by applying Unit.unit to both sides
All goals completed! π
Exercise 9 (p. 293)
For any map {X \xrightarrow{f} Y} there is a unique section \Gamma of p_X for which {f = p_Y \Gamma}, namely {\Gamma = \langle ?, f \rangle}.
Solution: Exercise 9
The unique section is {\Gamma = \langle 1_X, f \rangle}.
example {π : Type u} [Category.{v, u} π]
(X Y : π) [HasBinaryProduct X Y] :
β f : X βΆ Y,
β! Ξ : SplitEpi prod.fst, f = prod.snd β Ξ.section_ := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πinstβ:HasBinaryProduct X Yβ’ β (f : X βΆ Y), β! Ξ, f = prod.snd β Ξ.section_
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πinstβ:HasBinaryProduct X Yf:X βΆ Yβ’ β! Ξ, f = prod.snd β Ξ.section_
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πinstβ:HasBinaryProduct X Yf:X βΆ Yβ’ (fun Ξ β¦ f = prod.snd β Ξ.section_) { section_ := prod.lift (π X) f, id := β― } β§
β (y : SplitEpi prod.fst), (fun Ξ β¦ f = prod.snd β Ξ.section_) y β y = { section_ := prod.lift (π X) f, id := β― }
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πinstβ:HasBinaryProduct X Yf:X βΆ Yβ’ (fun Ξ β¦ f = prod.snd β Ξ.section_) { section_ := prod.lift (π X) f, id := β― }π:Type uinstβΒΉ:Category.{v, u} πX:πY:πinstβ:HasBinaryProduct X Yf:X βΆ Yβ’ β (y : SplitEpi prod.fst), (fun Ξ β¦ f = prod.snd β Ξ.section_) y β y = { section_ := prod.lift (π X) f, id := β― }
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πinstβ:HasBinaryProduct X Yf:X βΆ Yβ’ (fun Ξ β¦ f = prod.snd β Ξ.section_) { section_ := prod.lift (π X) f, id := β― } All goals completed! π
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πinstβ:HasBinaryProduct X Yf:X βΆ Yβ’ β (y : SplitEpi prod.fst), (fun Ξ β¦ f = prod.snd β Ξ.section_) y β y = { section_ := prod.lift (π X) f, id := β― } intro Ξ' π:Type uinstβΒΉ:Category.{v, u} πX:πY:πinstβ:HasBinaryProduct X Yf:X βΆ YΞ':SplitEpi prod.fsthf:f = prod.snd β Ξ'.section_β’ Ξ' = { section_ := prod.lift (π X) f, id := β― }
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πinstβ:HasBinaryProduct X Yf:X βΆ YΞ':SplitEpi prod.fsthf:f = prod.snd β Ξ'.section_β’ prod.fst β Ξ'.section_ = prod.fst β { section_ := prod.lift (π X) f, id := β― }.section_π:Type uinstβΒΉ:Category.{v, u} πX:πY:πinstβ:HasBinaryProduct X Yf:X βΆ YΞ':SplitEpi prod.fsthf:f = prod.snd β Ξ'.section_β’ prod.snd β Ξ'.section_ = prod.snd β { section_ := prod.lift (π X) f, id := β― }.section_
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πinstβ:HasBinaryProduct X Yf:X βΆ YΞ':SplitEpi prod.fsthf:f = prod.snd β Ξ'.section_β’ prod.fst β Ξ'.section_ = prod.fst β { section_ := prod.lift (π X) f, id := β― }.section_ All goals completed! π
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πinstβ:HasBinaryProduct X Yf:X βΆ YΞ':SplitEpi prod.fsthf:f = prod.snd β Ξ'.section_β’ prod.snd β Ξ'.section_ = prod.snd β { section_ := prod.lift (π X) f, id := β― }.section_ All goals completed! π
Exercise 10 (p. 294)
Given two parallel maps {X \xrightarrow{f} Y}, {X \xrightarrow{g} Y} in a category with products (such as πΊ), consider their graphs \Gamma_f and \Gamma_g. Explain pictorially why the equalizer of {f, g} is isomorphic to the intersection in {X \times Y} of their graphs.
Solution: Exercise 10
We provide two formalisations of the proof that the equalizer of {f, g} is isomorphic to the intersection in {X \times Y} of their graphs. The first proof uses the book definition of equalizer and a manual definition of intersection (since the book has not yet introduced the concept of an intersection). The second uses mathlib's API for equalizers and pullbacks, the latter being how intersections are implemented in mathlib. We have kept the structure of the two proofs essentially the same to aid in undertanding the translation between manual terms and API terms.
The 'manual' proof is as follows:
example {π : Type u} [Category.{v, u} π]
(X Y : π) (f g : X βΆ Y) [HasBinaryProduct X Y]
-- Equalizer of f, g
(Eβ : π) (p : Eβ βΆ X) (hp : f β p = g β p)
(liftβ : β {T : π} (x : T βΆ X), f β x = g β x β (T βΆ Eβ))
(facβ : β {T : π} (x : T βΆ X) (h : f β x = g β x),
p β liftβ x h = x)
(uniqβ : β {T : π} (x : T βΆ X) (h : f β x = g β x)
(m : T βΆ Eβ), p β m = x β m = liftβ x h)
-- Graphs of f and g
(Ξf Ξg : SplitEpi prod.fst)
(hΞf : f = prod.snd β Ξf.section_)
(hΞg : g = prod.snd β Ξg.section_)
-- Intersection in X Γ Y of graphs of f and g
(Eβ : π) (u : Eβ βΆ X) (v : Eβ βΆ X)
(h_intersect : Ξf.section_ β u = Ξg.section_ β v)
(liftβ : β {T : π} (u' v' : T βΆ X),
Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ))
(fac_uβ : β {T : π} (u' v' : T βΆ X)
(h : Ξf.section_ β u' = Ξg.section_ β v'),
u β liftβ u' v' h = u')
(_ : β {T : π} (u' v' : T βΆ X)
(h : Ξf.section_ β u' = Ξg.section_ β v'),
v β liftβ u' v' h = v')
(uniqβ : β {T : π} (u' v' : T βΆ X)
(h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' h) :
Eβ β
Eβ := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hβ’ Eβ β
Eβ
have huv : u = v := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hβ’ Eβ β
Eβ
calc
u = π X β u := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hβ’ u = π X β u All goals completed! π
_ = (prod.fst β Ξf.section_) β u := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hβ’ π X β u = (prod.fst β Ξf.section_) β u All goals completed! π
_ = prod.fst β (Ξf.section_ β u) := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hβ’ (prod.fst β Ξf.section_) β u = prod.fst β Ξf.section_ β u All goals completed! π
_ = prod.fst β (Ξg.section_ β v) := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hβ’ prod.fst β Ξf.section_ β u = prod.fst β Ξg.section_ β v All goals completed! π
_ = (prod.fst β Ξg.section_) β v := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hβ’ prod.fst β Ξg.section_ β v = (prod.fst β Ξg.section_) β v All goals completed! π
_ = π X β v := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hβ’ (prod.fst β Ξg.section_) β v = π X β v All goals completed! π
_ = v := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hβ’ π X β v = v All goals completed! π
have hu_eq : f β u = g β u := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hβ’ Eβ β
Eβ
calc f β u
_ = (prod.snd β Ξf.section_) β u := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vβ’ f β u = (prod.snd β Ξf.section_) β u All goals completed! π
_ = prod.snd β (Ξf.section_ β u) := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vβ’ (prod.snd β Ξf.section_) β u = prod.snd β Ξf.section_ β u All goals completed! π
_ = prod.snd β (Ξg.section_ β v) := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vβ’ prod.snd β Ξf.section_ β u = prod.snd β Ξg.section_ β v All goals completed! π
_ = (prod.snd β Ξg.section_) β v := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vβ’ prod.snd β Ξg.section_ β v = (prod.snd β Ξg.section_) β v All goals completed! π
_ = g β v := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vβ’ (prod.snd β Ξg.section_) β v = g β v All goals completed! π
_ = g β u := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vβ’ g β v = g β u All goals completed! π
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqβ’ Eβ β
Eβ
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uβ’ Eβ β
Eβ
have hp_eq : Ξf.section_ β p = Ξg.section_ β p := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hβ’ Eβ β
Eβ
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uβ’ prod.fst β Ξf.section_ β p = prod.fst β Ξg.section_ β pπ:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uβ’ prod.snd β Ξf.section_ β p = prod.snd β Ξg.section_ β p
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uβ’ prod.fst β Ξf.section_ β p = prod.fst β Ξg.section_ β p π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uβ’ p = prod.fst β Ξg.section_ β p
All goals completed! π
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uβ’ prod.snd β Ξf.section_ β p = prod.snd β Ξg.section_ β p All goals completed! π
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uhp_eq:Ξf.section_ β p = Ξg.section_ β peββ_lift:Eβ βΆ Eβ := liftβ p p hp_eqβ’ Eβ β
Eβ
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uhp_eq:Ξf.section_ β p = Ξg.section_ β peββ_lift:Eβ βΆ Eβ := liftβ p p hp_eqeββ_fac_u:u β liftβ p p hp_eq = pβ’ Eβ β
Eβ
exact {
hom := eββ_lift
inv := eββ_lift
hom_inv_id := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uhp_eq:Ξf.section_ β p = Ξg.section_ β peββ_lift:Eβ βΆ Eβ := liftβ p p hp_eqeββ_fac_u:u β liftβ p p hp_eq = pβ’ eββ_lift β eββ_lift = π Eβ
have h : p β eββ_lift β eββ_lift = p := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uhp_eq:Ξf.section_ β p = Ξg.section_ β peββ_lift:Eβ βΆ Eβ := liftβ p p hp_eqeββ_fac_u:u β liftβ p p hp_eq = pβ’ eββ_lift β eββ_lift = π Eβ
All goals completed! π
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uhp_eq:Ξf.section_ β p = Ξg.section_ β peββ_lift:Eβ βΆ Eβ := liftβ p p hp_eqeββ_fac_u:u β liftβ p p hp_eq = ph:p β eββ_lift β eββ_lift = phβ:π Eβ = liftβ p hpβ’ eββ_lift β eββ_lift = π Eβ
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uhp_eq:Ξf.section_ β p = Ξg.section_ β peββ_lift:Eβ βΆ Eβ := liftβ p p hp_eqeββ_fac_u:u β liftβ p p hp_eq = ph:p β eββ_lift β eββ_lift = phβ:π Eβ = liftβ p hphβ:eββ_lift β eββ_lift = liftβ p hpβ’ eββ_lift β eββ_lift = π Eβ
All goals completed! π
inv_hom_id := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uhp_eq:Ξf.section_ β p = Ξg.section_ β peββ_lift:Eβ βΆ Eβ := liftβ p p hp_eqeββ_fac_u:u β liftβ p p hp_eq = pβ’ eββ_lift β eββ_lift = π Eβ
have hu : u β eββ_lift β eββ_lift = u := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uhp_eq:Ξf.section_ β p = Ξg.section_ β peββ_lift:Eβ βΆ Eβ := liftβ p p hp_eqeββ_fac_u:u β liftβ p p hp_eq = pβ’ eββ_lift β eββ_lift = π Eβ
All goals completed! π
have hv : v β eββ_lift β eββ_lift = v := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uhp_eq:Ξf.section_ β p = Ξg.section_ β peββ_lift:Eβ βΆ Eβ := liftβ p p hp_eqeββ_fac_u:u β liftβ p p hp_eq = pβ’ eββ_lift β eββ_lift = π Eβ
All goals completed! π
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uhp_eq:Ξf.section_ β p = Ξg.section_ β peββ_lift:Eβ βΆ Eβ := liftβ p p hp_eqeββ_fac_u:u β liftβ p p hp_eq = phu:u β eββ_lift β eββ_lift = uhv:v β eββ_lift β eββ_lift = vhβ:π Eβ = liftβ u v h_intersectβ’ eββ_lift β eββ_lift = π Eβ
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasBinaryProduct X YEβ:πp:Eβ βΆ Xhp:f β p = g β pliftβ:{T : π} β (x : T βΆ X) β f β x = g β x β (T βΆ Eβ)facβ:β {T : π} (x : T βΆ X) (h : f β x = g β x), p β liftβ x h = xuniqβ:β {T : π} (x : T βΆ X) (h : f β x = g β x) (m : T βΆ Eβ), p β m = x β m = liftβ x hΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_Eβ:πu:Eβ βΆ Xv:Eβ βΆ Xh_intersect:Ξf.section_ β u = Ξg.section_ β vliftβ:{T : π} β (u' v' : T βΆ X) β Ξf.section_ β u' = Ξg.section_ β v' β (T βΆ Eβ)fac_uβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), u β liftβ u' v' h = u'xβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v'), v β liftβ u' v' h = v'uniqβ:β {T : π} (u' v' : T βΆ X) (h : Ξf.section_ β u' = Ξg.section_ β v') (m : T βΆ Eβ),
u β m = u' β v β m = v' β m = liftβ u' v' hhuv:u = vhu_eq:f β u = g β ueββ_lift:Eβ βΆ Eβ := liftβ u hu_eqheββ_fac:p β liftβ u hu_eq = uhp_eq:Ξf.section_ β p = Ξg.section_ β peββ_lift:Eβ βΆ Eβ := liftβ p p hp_eqeββ_fac_u:u β liftβ p p hp_eq = phu:u β eββ_lift β eββ_lift = uhv:v β eββ_lift β eββ_lift = vhβ:π Eβ = liftβ u v h_intersecthβ:eββ_lift β eββ_lift = liftβ u v h_intersectβ’ eββ_lift β eββ_lift = π Eβ
All goals completed! π
}
The API proof is as follows:
noncomputable example {π : Type u} [Category.{v, u} π]
(X Y : π) (f g : X βΆ Y) [HasBinaryProduct X Y]
-- Equalizer of f, g
[HasEqualizer f g]
-- Graphs of f and g
(Ξf Ξg : SplitEpi prod.fst)
(hΞf : f = prod.snd β Ξf.section_)
(hΞg : g = prod.snd β Ξg.section_)
-- Intersection in X Γ Y of graphs of f and g
[HasPullback Ξf.section_ Ξg.section_] :
equalizer f g β
pullback Ξf.section_ Ξg.section_ := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_β’ equalizer f g β
pullback Ξf.section_ Ξg.section_
π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gβ’ equalizer f g β
pullback Ξf.section_ Ξg.section_
π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_β’ equalizer f g β
pullback Ξf.section_ Ξg.section_
π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_β’ equalizer f g β
pullback Ξf.section_ Ξg.section_
have huv : u = v := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_β’ equalizer f g β
pullback Ξf.section_ Ξg.section_
calc
u = π X β u := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_β’ u = π X β u All goals completed! π
_ = (prod.fst β Ξf.section_) β u := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_β’ π X β u = (prod.fst β Ξf.section_) β u All goals completed! π
_ = prod.fst β (Ξf.section_ β u) := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_β’ (prod.fst β Ξf.section_) β u = prod.fst β Ξf.section_ β u All goals completed! π
_ = prod.fst β (Ξg.section_ β v) := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_β’ prod.fst β Ξf.section_ β u = prod.fst β Ξg.section_ β v All goals completed! π
_ = (prod.fst β Ξg.section_) β v := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_β’ prod.fst β Ξg.section_ β v = (prod.fst β Ξg.section_) β v All goals completed! π
_ = π X β v := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_β’ (prod.fst β Ξg.section_) β v = π X β v All goals completed! π
_ = v := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_β’ π X β v = v All goals completed! π
have hu_eq : f β u = g β u := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_β’ equalizer f g β
pullback Ξf.section_ Ξg.section_
calc f β u
_ = (prod.snd β Ξf.section_) β u := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vβ’ f β u = (prod.snd β Ξf.section_) β u All goals completed! π
_ = prod.snd β (Ξf.section_ β u) := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vβ’ (prod.snd β Ξf.section_) β u = prod.snd β Ξf.section_ β u All goals completed! π
_ = prod.snd β (Ξg.section_ β v) := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vβ’ prod.snd β Ξf.section_ β u = prod.snd β Ξg.section_ β v All goals completed! π
_ = (prod.snd β Ξg.section_) β v := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vβ’ prod.snd β Ξg.section_ β v = (prod.snd β Ξg.section_) β v All goals completed! π
_ = g β v := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vβ’ (prod.snd β Ξg.section_) β v = g β v All goals completed! π
_ = g β u := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vβ’ g β v = g β u All goals completed! π
have hp_eq : Ξf.section_ β p = Ξg.section_ β p := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_β’ equalizer f g β
pullback Ξf.section_ Ξg.section_
π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vhu_eq:f β u = g β uβ’ prod.fst β Ξf.section_ β p = prod.fst β Ξg.section_ β pπ:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vhu_eq:f β u = g β uβ’ prod.snd β Ξf.section_ β p = prod.snd β Ξg.section_ β p
π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vhu_eq:f β u = g β uβ’ prod.fst β Ξf.section_ β p = prod.fst β Ξg.section_ β p π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vhu_eq:f β u = g β uβ’ p = prod.fst β Ξg.section_ β p
All goals completed! π
π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vhu_eq:f β u = g β uβ’ prod.snd β Ξf.section_ β p = prod.snd β Ξg.section_ β p All goals completed! π
exact {
hom := pullback.lift p p hp_eq
inv := equalizer.lift u hu_eq
hom_inv_id := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vhu_eq:f β u = g β uhp_eq:Ξf.section_ β p = Ξg.section_ β pβ’ equalizer.lift u hu_eq β pullback.lift p p hp_eq = π (equalizer f g)
π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vhu_eq:f β u = g β uhp_eq:Ξf.section_ β p = Ξg.section_ β pβ’ equalizer.ΞΉ f g β equalizer.lift u hu_eq β pullback.lift p p hp_eq = equalizer.ΞΉ f g β π (equalizer f g)
All goals completed! π
inv_hom_id := π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vhu_eq:f β u = g β uhp_eq:Ξf.section_ β p = Ξg.section_ β pβ’ pullback.lift p p hp_eq β equalizer.lift u hu_eq = π (pullback Ξf.section_ Ξg.section_)
π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vhu_eq:f β u = g β uhp_eq:Ξf.section_ β p = Ξg.section_ β pβ’ pullback.fst Ξf.section_ Ξg.section_ β pullback.lift p p hp_eq β equalizer.lift u hu_eq =
pullback.fst Ξf.section_ Ξg.section_ β π (pullback Ξf.section_ Ξg.section_)π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vhu_eq:f β u = g β uhp_eq:Ξf.section_ β p = Ξg.section_ β pβ’ pullback.snd Ξf.section_ Ξg.section_ β pullback.lift p p hp_eq β equalizer.lift u hu_eq =
pullback.snd Ξf.section_ Ξg.section_ β π (pullback Ξf.section_ Ξg.section_)
π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vhu_eq:f β u = g β uhp_eq:Ξf.section_ β p = Ξg.section_ β pβ’ pullback.fst Ξf.section_ Ξg.section_ β pullback.lift p p hp_eq β equalizer.lift u hu_eq =
pullback.fst Ξf.section_ Ξg.section_ β π (pullback Ξf.section_ Ξg.section_) All goals completed! π
π:Type uinstβΒ³:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YinstβΒ²:HasBinaryProduct X YinstβΒΉ:HasEqualizer f gΞf:SplitEpi prod.fstΞg:SplitEpi prod.fsthΞf:f = prod.snd β Ξf.section_hΞg:g = prod.snd β Ξg.section_instβ:HasPullback Ξf.section_ Ξg.section_p:equalizer f g βΆ X := equalizer.ΞΉ f gu:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.fst Ξf.section_ Ξg.section_v:pullback Ξf.section_ Ξg.section_ βΆ X := pullback.snd Ξf.section_ Ξg.section_huv:u = vhu_eq:f β u = g β uhp_eq:Ξf.section_ β p = Ξg.section_ β pβ’ pullback.snd Ξf.section_ Ξg.section_ β pullback.lift p p hp_eq β equalizer.lift u hu_eq =
pullback.snd Ξf.section_ Ξg.section_ β π (pullback Ξf.section_ Ξg.section_) All goals completed! π
}
Between Exercises 10 and 11, the book discusses cographs and coequalizers.
To emphasize the duality between graphs and cographs, we first provide a formalisation of graph of f (cf. Exercise 9).
noncomputable def graphOf {π : Type u} [Category.{v, u} π]
{X Y : π} [HasBinaryProduct X Y] (f : X βΆ Y) : X βΆ X β¨― Y :=
prod.lift (π X) f
lemma graphOf_is_section {π : Type u} [Category.{v, u} π]
{X Y : π} [HasBinaryProduct X Y] (f : X βΆ Y) :
prod.fst β graphOf f = π X :=
prod.lift_fst (π X) f
lemma graphOf_commutes {π : Type u} [Category.{v, u} π]
{X Y : π} [HasBinaryProduct X Y] (f : X βΆ Y) :
prod.snd β graphOf f = f :=
prod.lift_snd (π X) f
Dualizing the definition of graph of f then gives the following formalisation of cograph of g.
noncomputable def cographOf {π : Type u} [Category.{v, u} π]
{X Y : π} [HasBinaryCoproduct X Y] (g : Y βΆ X) : X β¨Ώ Y βΆ X :=
coprod.desc (π X) g
lemma cographOf_is_retraction {π : Type u} [Category.{v, u} π]
{X Y : π} [HasBinaryCoproduct X Y] (g : Y βΆ X) :
cographOf g β coprod.inl = π X :=
coprod.inl_desc (π X) g
lemma cographOf_commutes {π : Type u} [Category.{v, u} π]
{X Y : π} [HasBinaryCoproduct X Y] (g : Y βΆ X) :
cographOf g β coprod.inr = g :=
coprod.inr_desc (π X) g
Similarly, the definition of coequalizer is dual to that of equalizer. That is, {X \xrightarrow{q} C} is a coequalizer of {u, v} if {qu = qv} and for each {X \xrightarrow{t} T} for which {tu = tv}, there is exactly one {C \xrightarrow{c} T} for which {t = cq} (cf. the definition of equalizer above).
In mathlib, two parallel morphisms have a coequalizer if their parallel pair diagram has a colimit. We print the definition of HasCoequalizer below for reference.
#print HasCoequalizer
Exercise 11 (p. 294)
Say that {Y \xrightarrow{h} Z} is a cosolution of the co-equation represented by a given source/target structure {X \xrightarrow{f} Y}, {X \xrightarrow{g} Y} if {hf = hg}. Show that if such a cosolution h is universal, in the sense that any other cosolution {Y \xrightarrow{h'} Z'} can be uniquely expressed as {h' = qh}, then h is an epimorphism. (A universal cosolution is called a coequalizer of the pair {f, g}; in many categories every epimorphism is a coequalizer of some pair.)
Solution: Exercise 11
This exercise is the dual of Exercise 6, so our proof here is essentially the same but with all arrows reversed. Following the approach taken in Exercise 6, we provide formalisations using both the book definition of coequalizer and mathlib's HasCoequalizer type class.
example {π : Type u} [Category.{v, u} π]
(X Y : π) (f g : X βΆ Y) (Z : π)
(h : Y βΆ Z) (hhβ : h β f = h β g)
(hhβ : β (Z' : π) (h' : Y βΆ Z'), h' β f = h' β g β
β! q : Z βΆ Z', h' = q β h) :
Epi h := π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YZ:πh:Y βΆ Zhhβ:h β f = h β ghhβ:β (Z' : π) (h' : Y βΆ Z'), h' β f = h' β g β β! q, h' = q β hβ’ Epi h
π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YZ:πh:Y βΆ Zhhβ:h β f = h β ghhβ:β (Z' : π) (h' : Y βΆ Z'), h' β f = h' β g β β! q, h' = q β hβ’ β {Z_1 : π} (g h_1 : Z βΆ Z_1), g β h = h_1 β h β g = h_1
intro Z' π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YZ:πh:Y βΆ Zhhβ:h β f = h β ghhβ:β (Z' : π) (h' : Y βΆ Z'), h' β f = h' β g β β! q, h' = q β hZ':πqβ:Z βΆ Z'β’ β (h_1 : Z βΆ Z'), qβ β h = h_1 β h β qβ = h_1 π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YZ:πh:Y βΆ Zhhβ:h β f = h β ghhβ:β (Z' : π) (h' : Y βΆ Z'), h' β f = h' β g β β! q, h' = q β hZ':πqβ:Z βΆ Z'qβ:Z βΆ Z'β’ qβ β h = qβ β h β qβ = qβ π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YZ:πh:Y βΆ Zhhβ:h β f = h β ghhβ:β (Z' : π) (h' : Y βΆ Z'), h' β f = h' β g β β! q, h' = q β hZ':πqβ:Z βΆ Z'qβ:Z βΆ Z'h_eqβ:qβ β h = qβ β hβ’ qβ = qβ
have h_eqβ : (qβ β h) β f = (qβ β h) β g := π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YZ:πh:Y βΆ Zhhβ:h β f = h β ghhβ:β (Z' : π) (h' : Y βΆ Z'), h' β f = h' β g β β! q, h' = q β hβ’ Epi h
All goals completed! π
π:Type uinstβ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ YZ:πh:Y βΆ Zhhβ:h β f = h β ghhβ:β (Z' : π) (h' : Y βΆ Z'), h' β f = h' β g β β! q, h' = q β hZ':πqβ:Z βΆ Z'qβ:Z βΆ Z'h_eqβ:qβ β h = qβ β hh_eqβ:(qβ β h) β f = (qβ β h) β gwβ:Z βΆ Z'leftβ:qβ β h = wβ β hh_uniq:β (y : Z βΆ Z'), (fun q β¦ qβ β h = q β h) y β y = wββ’ qβ = qβ
All goals completed! π
example {π : Type u} [Category.{v, u} π]
(X Y : π) (f g : X βΆ Y) [HasCoequalizer f g] :
Epi (coequalizer.Ο f g) := π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasCoequalizer f gβ’ Epi (coequalizer.Ο f g)
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasCoequalizer f gh:Y βΆ coequalizer f g := coequalizer.Ο f gβ’ Epi (coequalizer.Ο f g)
π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasCoequalizer f gh:Y βΆ coequalizer f g := coequalizer.Ο f gβ’ β {Z : π} (g_1 h : coequalizer f g βΆ Z), g_1 β coequalizer.Ο f g = h β coequalizer.Ο f g β g_1 = h
intro Z' π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasCoequalizer f gh:Y βΆ coequalizer f g := coequalizer.Ο f gZ':πqβ:coequalizer f g βΆ Z'β’ β (h : coequalizer f g βΆ Z'), qβ β coequalizer.Ο f g = h β coequalizer.Ο f g β qβ = h π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasCoequalizer f gh:Y βΆ coequalizer f g := coequalizer.Ο f gZ':πqβ:coequalizer f g βΆ Z'qβ:coequalizer f g βΆ Z'β’ qβ β coequalizer.Ο f g = qβ β coequalizer.Ο f g β qβ = qβ π:Type uinstβΒΉ:Category.{v, u} πX:πY:πf:X βΆ Yg:X βΆ Yinstβ:HasCoequalizer f gh:Y βΆ coequalizer f g := coequalizer.Ο f gZ':πqβ:coequalizer f g βΆ Z'qβ:coequalizer f g βΆ Z'h_eq:qβ β coequalizer.Ο f g = qβ β coequalizer.Ο f gβ’ qβ = qβ
All goals completed! π
Exercise 12 (p. 294)
For a given map {Y \xrightarrow{h} Z}, consider all parallel pairs {X \xrightarrow{f} Y}, {X \xrightarrow{g} Y} (for various X) such that {hf = hg}. Formulate the notion of a universal such; call it X_h. Show that {X_h \rightrightarrows Y} is reflexive, symmetric, transitive, and jointly monomorphic. Here 'reflexive' you know from our discussion of directed graphs, 'symmetric' means there is an involution \sigma of X_h whose right action interchanges the universal f and g. 'Jointly monomorphic' means the map {X \rightarrow Y \times Y} with label {\langle f, g \rangle} is injective. 'Transitivity' involves a trio of test maps {T \rightarrow Y}. (An STM reflexive graph is called an equivalence relation on Y; in many categories every equivalence relation arises as the universal X_h, for some h.)
Solution: Exercise 12
We take each of the four properties in turn.
{X_h \rightrightarrows Y} is reflexive:
example {π : Type u} [Category.{v, u} π]
(Y Z : π) (h : Y βΆ Z)
(Xh : π) (f g : Xh βΆ Y) (_ : h β f = h β g)
(h_univ : β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β
β! u : X βΆ Xh, f β u = f' β§ g β u = g') :
β r : Y βΆ Xh, f β r = π Y β§ g β r = π Y := π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yxβ:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'β’ β r, f β r = π Y β§ g β r = π Y
π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yxβ:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'r:Y βΆ Xhhr_comm:f β r = π Y β§ g β r = π Yrightβ:β (y : Y βΆ Xh), (fun u β¦ f β u = π Y β§ g β u = π Y) y β y = rβ’ β r, f β r = π Y β§ g β r = π Y
All goals completed! π
{X_h \rightrightarrows Y} is symmetric:
example {π : Type u} [Category.{v, u} π]
(Y Z : π) (h : Y βΆ Z)
(Xh : π) (f g : Xh βΆ Y) (hh : h β f = h β g)
(h_univ : β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β
β! u : X βΆ Xh, f β u = f' β§ g β u = g') :
β Ο : Xh βΆ Xh,
Ο β Ο = π Xh β§ f β Ο = g β§ g β Ο = f := π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'β’ β Ο, Ο β Ο = π Xh β§ f β Ο = g β§ g β Ο = f
π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'Ο:Xh βΆ XhhΟ_comm:f β Ο = g β§ g β Ο = frightβ:β (y : Xh βΆ Xh), (fun u β¦ f β u = g β§ g β u = f) y β y = Οβ’ β Ο, Ο β Ο = π Xh β§ f β Ο = g β§ g β Ο = f
π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'Ο:Xh βΆ XhhΟ_comm:f β Ο = g β§ g β Ο = frightβ:β (y : Xh βΆ Xh), (fun u β¦ f β u = g β§ g β u = f) y β y = Οβ’ Ο β Ο = π Xh
π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'Ο:Xh βΆ XhhΟ_comm:f β Ο = g β§ g β Ο = frightβ:β (y : Xh βΆ Xh), (fun u β¦ f β u = g β§ g β u = f) y β y = Οwβ:Xh βΆ Xhleftβ:f β wβ = f β§ g β wβ = gh_uniq:β (y : Xh βΆ Xh), (fun u β¦ f β u = f β§ g β u = g) y β y = wββ’ Ο β Ο = π Xh
π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'Ο:Xh βΆ XhhΟ_comm:f β Ο = g β§ g β Ο = frightβ:β (y : Xh βΆ Xh), (fun u β¦ f β u = g β§ g β u = f) y β y = Οwβ:Xh βΆ Xhleftβ:f β wβ = f β§ g β wβ = gh_uniq:β (y : Xh βΆ Xh), (fun u β¦ f β u = f β§ g β u = g) y β y = wβh1Xh:π Xh = wββ’ Ο β Ο = π Xh
have hΟΟ : Ο β Ο = _ :=
h_uniq (Ο β Ο) (π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'Ο:Xh βΆ XhhΟ_comm:f β Ο = g β§ g β Ο = frightβ:β (y : Xh βΆ Xh), (fun u β¦ f β u = g β§ g β u = f) y β y = Οwβ:Xh βΆ Xhleftβ:f β wβ = f β§ g β wβ = gh_uniq:β (y : Xh βΆ Xh), (fun u β¦ f β u = f β§ g β u = g) y β y = wβh1Xh:π Xh = wββ’ (fun u β¦ f β u = f β§ g β u = g) (Ο β Ο)
π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'Ο:Xh βΆ XhhΟ_comm:f β Ο = g β§ g β Ο = frightβ:β (y : Xh βΆ Xh), (fun u β¦ f β u = g β§ g β u = f) y β y = Οwβ:Xh βΆ Xhleftβ:f β wβ = f β§ g β wβ = gh_uniq:β (y : Xh βΆ Xh), (fun u β¦ f β u = f β§ g β u = g) y β y = wβh1Xh:π Xh = wββ’ f β Ο β Ο = fπ:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'Ο:Xh βΆ XhhΟ_comm:f β Ο = g β§ g β Ο = frightβ:β (y : Xh βΆ Xh), (fun u β¦ f β u = g β§ g β u = f) y β y = Οwβ:Xh βΆ Xhleftβ:f β wβ = f β§ g β wβ = gh_uniq:β (y : Xh βΆ Xh), (fun u β¦ f β u = f β§ g β u = g) y β y = wβh1Xh:π Xh = wββ’ g β Ο β Ο = g
π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'Ο:Xh βΆ XhhΟ_comm:f β Ο = g β§ g β Ο = frightβ:β (y : Xh βΆ Xh), (fun u β¦ f β u = g β§ g β u = f) y β y = Οwβ:Xh βΆ Xhleftβ:f β wβ = f β§ g β wβ = gh_uniq:β (y : Xh βΆ Xh), (fun u β¦ f β u = f β§ g β u = g) y β y = wβh1Xh:π Xh = wββ’ f β Ο β Ο = f All goals completed! π
π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'Ο:Xh βΆ XhhΟ_comm:f β Ο = g β§ g β Ο = frightβ:β (y : Xh βΆ Xh), (fun u β¦ f β u = g β§ g β u = f) y β y = Οwβ:Xh βΆ Xhleftβ:f β wβ = f β§ g β wβ = gh_uniq:β (y : Xh βΆ Xh), (fun u β¦ f β u = f β§ g β u = g) y β y = wβh1Xh:π Xh = wββ’ g β Ο β Ο = g All goals completed! π)
All goals completed! π
{X_h \rightrightarrows Y} is transitive:
example {π : Type u} [Category.{v, u} π]
(Y Z : π) (h : Y βΆ Z)
(Xh : π) (f g : Xh βΆ Y) (hh : h β f = h β g)
(h_univ : β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β
β! u : X βΆ Xh, f β u = f' β§ g β u = g') :
β {T : π} (yβ yβ yβ : T βΆ Y) (vβ vβ : T βΆ Xh),
f β vβ = yβ β g β vβ = yβ β f β vβ = yβ β g β vβ = yβ β
β vβ : T βΆ Xh, f β vβ = yβ β§ g β vβ = yβ := π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'β’ β {T : π} (yβ yβ yβ : T βΆ Y) (vβ vβ : T βΆ Xh),
f β vβ = yβ β g β vβ = yβ β f β vβ = yβ β g β vβ = yβ β β vβ, f β vβ = yβ β§ g β vβ = yβ
intro T π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yβ’ β (yβ yβ : T βΆ Y) (vβ vβ : T βΆ Xh),
f β vβ = yβ β g β vβ = yβ β f β vβ = yβ β g β vβ = yβ β β vβ, f β vβ = yβ β§ g β vβ = yβ π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yβ’ β (yβ : T βΆ Y) (vβ vβ : T βΆ Xh), f β vβ = yβ β g β vβ = yβ β f β vβ = yβ β g β vβ = yβ β β vβ, f β vβ = yβ β§ g β vβ = yβ π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yβ’ β (vβ vβ : T βΆ Xh), f β vβ = yβ β g β vβ = yβ β f β vβ = yβ β g β vβ = yβ β β vβ, f β vβ = yβ β§ g β vβ = yβ π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhβ’ β (vβ : T βΆ Xh), f β vβ = yβ β g β vβ = yβ β f β vβ = yβ β g β vβ = yβ β β vβ, f β vβ = yβ β§ g β vβ = yβ π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhβ’ f β vβ = yβ β g β vβ = yβ β f β vβ = yβ β g β vβ = yβ β β vβ, f β vβ = yβ β§ g β vβ = yβ π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yββ’ g β vβ = yβ β f β vβ = yβ β g β vβ = yβ β β vβ, f β vβ = yβ β§ g β vβ = yβ π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yββ’ f β vβ = yβ β g β vβ = yβ β β vβ, f β vβ = yβ β§ g β vβ = yβ π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yβhfβ:f β vβ = yββ’ g β vβ = yβ β β vβ, f β vβ = yβ β§ g β vβ = yβ π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yβhfβ:f β vβ = yβhgβ:g β vβ = yββ’ β vβ, f β vβ = yβ β§ g β vβ = yβ
have hy : h β yβ = h β yβ := calc h β yβ
_ = h β (f β vβ) := π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yβhfβ:f β vβ = yβhgβ:g β vβ = yββ’ h β yβ = h β f β vβ All goals completed! π
_ = (h β f) β vβ := π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yβhfβ:f β vβ = yβhgβ:g β vβ = yββ’ h β f β vβ = (h β f) β vβ All goals completed! π
_ = (h β g) β vβ := π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yβhfβ:f β vβ = yβhgβ:g β vβ = yββ’ (h β f) β vβ = (h β g) β vβ All goals completed! π
_ = h β (g β vβ) := π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yβhfβ:f β vβ = yβhgβ:g β vβ = yββ’ (h β g) β vβ = h β g β vβ All goals completed! π
_ = h β yβ := π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yβhfβ:f β vβ = yβhgβ:g β vβ = yββ’ h β g β vβ = h β yβ All goals completed! π
_ = h β (f β vβ) := π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yβhfβ:f β vβ = yβhgβ:g β vβ = yββ’ h β yβ = h β f β vβ All goals completed! π
_ = (h β f) β vβ := π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yβhfβ:f β vβ = yβhgβ:g β vβ = yββ’ h β f β vβ = (h β f) β vβ All goals completed! π
_ = (h β g) β vβ := π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yβhfβ:f β vβ = yβhgβ:g β vβ = yββ’ (h β f) β vβ = (h β g) β vβ All goals completed! π
_ = h β (g β vβ) := π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yβhfβ:f β vβ = yβhgβ:g β vβ = yββ’ (h β g) β vβ = h β g β vβ All goals completed! π
_ = h β yβ := π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yβhfβ:f β vβ = yβhgβ:g β vβ = yββ’ h β g β vβ = h β yβ All goals completed! π
π:Type uinstβ:Category.{v, u} πY:πZ:πh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πyβ:T βΆ Yyβ:T βΆ Yyβ:T βΆ Yvβ:T βΆ Xhvβ:T βΆ Xhhfβ:f β vβ = yβhgβ:g β vβ = yβhfβ:f β vβ = yβhgβ:g β vβ = yβhy:h β yβ = h β yβvβ:T βΆ Xhleftβ:f β vβ = yβ β§ g β vβ = yβrightβ:β (y : T βΆ Xh), (fun u β¦ f β u = yβ β§ g β u = yβ) y β y = vββ’ β vβ, f β vβ = yβ β§ g β vβ = yβ
All goals completed! π
{X_h \rightrightarrows Y} is jointly monomorphic:
example {π : Type u} [Category.{v, u} π]
(Y Z : π) [HasBinaryProduct Y Y] (h : Y βΆ Z)
(Xh : π) (f g : Xh βΆ Y) (hh : h β f = h β g)
(h_univ : β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β
β! u : X βΆ Xh, f β u = f' β§ g β u = g') :
β {T : π} (a b : T βΆ Xh),
prod.lift f g β a = prod.lift f g β b β a = b := π:Type uinstβΒΉ:Category.{v, u} πY:πZ:πinstβ:HasBinaryProduct Y Yh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'β’ β {T : π} (a b : T βΆ Xh), prod.lift f g β a = prod.lift f g β b β a = b
intro T π:Type uinstβΒΉ:Category.{v, u} πY:πZ:πinstβ:HasBinaryProduct Y Yh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πa:T βΆ Xhβ’ β (b : T βΆ Xh), prod.lift f g β a = prod.lift f g β b β a = b π:Type uinstβΒΉ:Category.{v, u} πY:πZ:πinstβ:HasBinaryProduct Y Yh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πa:T βΆ Xhb:T βΆ Xhβ’ prod.lift f g β a = prod.lift f g β b β a = b π:Type uinstβΒΉ:Category.{v, u} πY:πZ:πinstβ:HasBinaryProduct Y Yh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πa:T βΆ Xhb:T βΆ Xhhp_comm:prod.lift f g β a = prod.lift f g β bβ’ a = b
have hf : f β a = f β b := π:Type uinstβΒΉ:Category.{v, u} πY:πZ:πinstβ:HasBinaryProduct Y Yh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'β’ β {T : π} (a b : T βΆ Xh), prod.lift f g β a = prod.lift f g β b β a = b
All goals completed! π
have hg : g β a = g β b := π:Type uinstβΒΉ:Category.{v, u} πY:πZ:πinstβ:HasBinaryProduct Y Yh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'β’ β {T : π} (a b : T βΆ Xh), prod.lift f g β a = prod.lift f g β b β a = b
All goals completed! π
obtain β¨_, _, h_uniqβ© := h_univ (f β a) (g β a) (π:Type uinstβΒΉ:Category.{v, u} πY:πZ:πinstβ:HasBinaryProduct Y Yh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πa:T βΆ Xhb:T βΆ Xhhp_comm:prod.lift f g β a = prod.lift f g β bhf:f β a = f β bhg:g β a = g β bβ’ h β f β a = h β g β a
All goals completed! π)
π:Type uinstβΒΉ:Category.{v, u} πY:πZ:πinstβ:HasBinaryProduct Y Yh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πa:T βΆ Xhb:T βΆ Xhhp_comm:prod.lift f g β a = prod.lift f g β bhf:f β a = f β bhg:g β a = g β bwβ:T βΆ Xhleftβ:f β wβ = f β a β§ g β wβ = g β ah_uniq:β (y : T βΆ Xh), (fun u β¦ f β u = f β a β§ g β u = g β a) y β y = wβha:a = wββ’ a = b
π:Type uinstβΒΉ:Category.{v, u} πY:πZ:πinstβ:HasBinaryProduct Y Yh:Y βΆ ZXh:πf:Xh βΆ Yg:Xh βΆ Yhh:h β f = h β gh_univ:β {X : π} (f' g' : X βΆ Y), h β f' = h β g' β β! u, f β u = f' β§ g β u = g'T:πa:T βΆ Xhb:T βΆ Xhhp_comm:prod.lift f g β a = prod.lift f g β bhf:f β a = f β bhg:g β a = g β bwβ:T βΆ Xhleftβ:f β wβ = f β a β§ g β wβ = g β ah_uniq:β (y : T βΆ Xh), (fun u β¦ f β u = f β a β§ g β u = g β a) y β y = wβha:a = wβhb:b = wββ’ a = b
All goals completed! π