CategoryTheory.EffectiveEpi.uniq
theorem CategoryTheory.EffectiveEpi.uniq :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y W : C} (f : Y ⟶ X)
[inst_1 : CategoryTheory.EffectiveEpi f] (e : Y ⟶ W)
(h :
∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e)
(m : X ⟶ W), CategoryTheory.CategoryStruct.comp f m = e → m = CategoryTheory.EffectiveEpi.desc f e ⋯
The theorem `CategoryTheory.EffectiveEpi.uniq` in Lean 4 states that for any category $C$, given objects $X$, $Y$, and $W$ in $C$, a morphism $f: Y \to X$ that is an effective epimorphism, and a morphism $e: Y \to W$. If for all objects $Z$ in $C$, and for any two morphisms $g_1, g_2: Z \to Y$, the situation where the composition of $g_1$ and $f$ is equal to the composition of $g_2$ and $f$ implies that the composition of $g_1$ and $e$ is equal to the composition of $g_2$ and $e$, then for any morphism $m: X \to W$ such that its composition with $f$ equals to $e$, $m$ is equal to the desc morphism of $f$ and $e$. In simple terms, under the given conditions, the morphism $m$ is uniquely determined by the effective epimorphism and the morphism $e$.
More concisely: Given any category $C$, if $f: Y \to X$ is an effective epimorphism and for all $Z$ and morphisms $g\_1, g\_2: Z \to Y$, $g\_1 \circ f = g\_2 \circ f$ implies $g\_1 \circ e = g\_2 \circ e$, then the description morphism of $f$ and $e$ is unique.
|
CategoryTheory.EffectiveEpiFamily.uniq
theorem CategoryTheory.EffectiveEpiFamily.uniq :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {B W : C} {α : Type u_2} (X : α → C)
(π : (a : α) → X a ⟶ B) [inst_1 : CategoryTheory.EffectiveEpiFamily X π] (e : (a : α) → X a ⟶ W)
(h :
∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
(m : B ⟶ W),
(∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) →
m = CategoryTheory.EffectiveEpiFamily.desc X π e ⋯
This theorem, `CategoryTheory.EffectiveEpiFamily.uniq`, states that in a category `C`, for any objects `B` and `W`, and a family of objects `X` indexed by `α`, with morphisms `π` from each `X a` to `B`, if this family forms an effective epimorphism, and there exist morphisms `e` from each `X a` to `W` such that for any object `Z` in `C` and any morphisms `g₁` and `g₂` from `Z` to `X a₁` and `X a₂` respectively, if the compositions `g₁ ≫ π a₁` and `g₂ ≫ π a₂` are equal then the compositions `g₁ ≫ e a₁` and `g₂ ≫ e a₂` are also equal, then for any morphism `m` from `B` to `W` that makes `π a ≫ m` equal to `e a` for all `a` in `α`, `m` must be equal to the unique morphism described by `CategoryTheory.EffectiveEpiFamily.desc X π e`.
In simpler terms, it says that in a category, if we have a family of objects and morphisms that behave like a collective "epimorphism", and there exists a certain commutative diagram, then any morphism that composes with the family to recreate this diagram must be the unique morphism described by a specific construction in category theory.
More concisely: Given a category `C`, an effective epimorphism `π : ⨅α, Xα → B` of objects in `C`, and morphisms `e : ⨅α, Xα → W` such that for any `g₁, g₂ : C → Xα₁, α₂` with `g₁ ≫ πα₁ = g₂ ≫ πα₂` implying `g₁ ≫ eα₁ = g₂ ≫ eα₂`, there exists a unique morphism `m : B → W` satisfying `π a ≫ m = e a` for all `a ∈ α`, such that for all `h : C → W`, if `h ≫ π = m`, then `h = CategoryTheory.EffectiveEpiFamily.desc X π e`.
|
CategoryTheory.EffectiveEpiFamily.fac
theorem CategoryTheory.EffectiveEpiFamily.fac :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {B W : C} {α : Type u_2} (X : α → C)
(π : (a : α) → X a ⟶ B) [inst_1 : CategoryTheory.EffectiveEpiFamily X π] (e : (a : α) → X a ⟶ W)
(h :
∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
(a : α), CategoryTheory.CategoryStruct.comp (π a) (CategoryTheory.EffectiveEpiFamily.desc X π e ⋯) = e a
This theorem, named `CategoryTheory.EffectiveEpiFamily.fac`, is from the field of category theory. Given a category `C`, with objects `B` and `W` and a type `α`, it considers a family of morphisms `X : α → C` and `π : (a : α) → X a ⟶ B` that forms an effective epimorphism family. It also takes a morphism `e : (a : α) → X a ⟶ W` that satisfies a property denoted by `h`. This property ensures that, for all objects `Z` in `C` and all elements `a₁, a₂` of `α`, if the composition of two morphisms `g₁ : Z ⟶ X a₁` and `g₂ : Z ⟶ X a₂` with `π a₁` and `π a₂` respectively are equal, then the compositions of `g₁` and `g₂` with `e a₁` and `e a₂` respectively are also equal. The theorem then states that for any `a : α`, the composition of `π a` with the morphism given by the `desc` operation of the effective epimorphism family `X π` applied to `e` is equal to `e a`.
More concisely: Given a category `C`, a family `X : α → C` and morphism `π : α → X �Circ B` forming an effective epimorphism family, and a morphism `e : α → X �Circ W` satisfying a certain condition, for all objects `Z` in `C` and all `a` in `α`, the composition of `π a` with the `desc` morphism of `X π` applied to `e` at `a` equals `e a`.
|