CategoryTheory.StrongEpiCategory.strongEpi_of_epi
theorem CategoryTheory.StrongEpiCategory.strongEpi_of_epi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.StrongEpiCategory C] {X Y : C}
(f : X ⟶ Y) [inst_1 : CategoryTheory.Epi f], CategoryTheory.StrongEpi f
This theorem declares that in a strong epimorphism category (a category where all epimorphisms are strong), any morphism 'f' from object X to object Y, if it is an epimorphism, is also a strong epimorphism. Here, 'strong epimorphism' is a condition on a morphism in a category that is stronger than being an epimorphism (a morphism where pre-composition is a right cancelable operation). The theorem is universal, applying to any objects X and Y in the category and any morphism 'f' between them.
More concisely: In a strong epimorphism category, every epimorphism is a strong epimorphism.
|
CategoryTheory.strongMono_comp
theorem CategoryTheory.strongMono_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R)
[inst_1 : CategoryTheory.StrongMono f] [inst_2 : CategoryTheory.StrongMono g],
CategoryTheory.StrongMono (CategoryTheory.CategoryStruct.comp f g)
The theorem `CategoryTheory.strongMono_comp` states that, in any category `C`, if `f` is a strong monomorphism from object `P` to `Q`, and `g` is a strong monomorphism from object `Q` to `R`, then the composition of `f` and `g` (denoted by `CategoryTheory.CategoryStruct.comp f g`), is also a strong monomorphism. Here, `P`, `Q`, and `R` are objects in the category `C`. This is a property about the composability of strong monomorphisms in category theory.
More concisely: If `f` is a strong monomorphism from object `P` to `Q` and `g` is a strong monomorphism from object `Q` to `R` in a category `C`, then their composition `g ∘ f` is a strong monomorphism from `P` to `R`.
|
CategoryTheory.StrongEpi.llp
theorem CategoryTheory.StrongEpi.llp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} {f : P ⟶ Q} [self : CategoryTheory.StrongEpi f]
⦃X Y : C⦄ (z : X ⟶ Y) [inst_1 : CategoryTheory.Mono z], CategoryTheory.HasLiftingProperty f z
This theorem is about the left lifting property in category theory. It states that for any category `C`, and any objects `P`, `Q`, `X`, `Y` in `C`, if `f` is a morphism from `P` to `Q` and `f` is a strong epimorphism, and if `z` is a morphism from `X` to `Y` and `z` is a monomorphism, then `f` has the left lifting property with respect to `z`. The left lifting property is a fundamental concept in category theory and is used in various constructions and proofs.
More concisely: In any category `C`, given objects `P`, `Q`, `X`, `Y`, a strong epimorphism `f` from `P` to `Q`, and a monomorphism `z` from `X` to `Y`, there exists a morphism `h` from `X` to `P` such that `f ∘ h = z`.
|
CategoryTheory.StrongMono.mono
theorem CategoryTheory.StrongMono.mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} {f : P ⟶ Q} [self : CategoryTheory.StrongMono f],
CategoryTheory.Mono f
This theorem is about the concept of monomorphisms in category theory. Specifically, it states that for any category `C` and any objects `P` and `Q` in `C`, if a morphism `f` from `P` to `Q` is a strong monomorphism (as indicated by `CategoryTheory.StrongMono f`), then `f` is also a monomorphism. This is expressed within the context of the Lean 4 formal proof management system, which allows mathematical concepts and relationships to be precisely defined and proven.
More concisely: In any category, a strong monomorphism is a morphism that is left-inverting with all its right kernel arrows, and thus is a monomorphism.
|
CategoryTheory.strongEpi_comp
theorem CategoryTheory.strongEpi_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R)
[inst_1 : CategoryTheory.StrongEpi f] [inst_2 : CategoryTheory.StrongEpi g],
CategoryTheory.StrongEpi (CategoryTheory.CategoryStruct.comp f g)
This theorem states that in any category 'C', if we have three objects P, Q, and R and two morphisms `f` from P to Q and `g` from Q to R, then if both `f` and `g` are strong epimorphisms, the composition of `f` and `g` (denoted as `CategoryTheory.CategoryStruct.comp f g`) is also a strong epimorphism. An epimorphism is a morphism where for all morphisms that follow it, equal composition results in equal morphisms, and a strong epimorphism is a kind of epimorphism that has a certain property related to the pullback.
More concisely: In any category, if two strong epimorphisms compose, the resulting morphism is also a strong epimorphism.
|
CategoryTheory.StrongMono.rlp
theorem CategoryTheory.StrongMono.rlp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} {f : P ⟶ Q} [self : CategoryTheory.StrongMono f]
⦃X Y : C⦄ (z : X ⟶ Y) [inst_1 : CategoryTheory.Epi z], CategoryTheory.HasLiftingProperty z f
This theorem states that in any category `C`, for any objects `P` and `Q` in `C` and for any morphism `f` from `P` to `Q` which is a strong monomorphism, then for any two objects `X` and `Y` in `C` and any morphism `z` from `X` to `Y` which is an epimorphism, `f` has the right lifting property with respect to `z`. This means that for every commutative square with `z` and `f` as two of its sides, there exists a diagonal morphism that makes the two resulting triangles commute.
More concisely: In any category `C`, given objects `P`, `Q`, a strong monomorphism `f` from `P` to `Q`, and an epimorphism `z` from `X` to `Y`, the square commuting diagram with `z` and `f` as sides has a diagonal filling morphism making both triangles commute.
|
CategoryTheory.StrongEpi.epi
theorem CategoryTheory.StrongEpi.epi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} {f : P ⟶ Q} [self : CategoryTheory.StrongEpi f],
CategoryTheory.Epi f
This theorem states that for any category `C` of type `u`, any two objects `P` and `Q` in `C`, and a morphism `f` from `P` to `Q`, if `f` is a strong epimorphism, meaning that it satisfies certain conditions related to the composition of morphisms, then `f` is also an epimorphism, which means it is a function that satisfies the right cancellation property in the category.
More concisely: In any category, a strong epimorphism is an epimorphism.
|
CategoryTheory.strongMono_of_strongMono
theorem CategoryTheory.strongMono_of_strongMono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R)
[inst_1 : CategoryTheory.StrongMono (CategoryTheory.CategoryStruct.comp f g)], CategoryTheory.StrongMono f
The theorem `CategoryTheory.strongMono_of_strongMono` states that in any category `C`, if the composition of two morphisms `f` and `g` (denoted as `f ≫ g`) is a strong monomorphism, then the morphism `f` is also a strong monomorphism. Here, `f` is a morphism from object `P` to `Q`, and `g` is a morphism from `Q` to `R`. A strong monomorphism is a specific kind of morphism in category theory that has certain injective properties.
More concisely: If `f ≫ g` is a strong monomorphism in a category `C`, then `f` is a strong monomorphism from `P` to `Q`.
|
CategoryTheory.strongEpi_of_strongEpi
theorem CategoryTheory.strongEpi_of_strongEpi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R)
[inst_1 : CategoryTheory.StrongEpi (CategoryTheory.CategoryStruct.comp f g)], CategoryTheory.StrongEpi g
The theorem `CategoryTheory.strongEpi_of_strongEpi` states that in any category `C`, for any three objects `P`, `Q`, and `R` in `C`, if the composition of two morphisms `f : P ⟶ Q` and `g : Q ⟶ R` (notated as `f ≫ g`) is a strong epimorphism, then the morphism `g` is also a strong epimorphism. Here, a strong epimorphism is a special type of morphism in category theory that has certain properties related to the existence of certain kinds of diagrams.
More concisely: If `f : P ⟶ Q` and `g : Q ⟶ R` are morphisms in a category `C` such that `f ≫ g` is a strong epimorphism, then `g` is also a strong epimorphism.
|
CategoryTheory.StrongMonoCategory.strongMono_of_mono
theorem CategoryTheory.StrongMonoCategory.strongMono_of_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.StrongMonoCategory C] {X Y : C}
(f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f], CategoryTheory.StrongMono f
This theorem states that in a strong mono category, every monomorphism is strong. In other words, for any category `C`, if `C` is a strong mono category and `f` is a morphism from object `X` to `Y` in `C` that is monic (i.e., a left-cancelable morphism), then `f` is a strong monomorphism. A strong monomorphism is a monopolized morphism which has the property of the lifting property for all commutative squares, a concept in category theory.
More concisely: In a strong mono category, every monomorphism is a strong monomorphism.
|
CategoryTheory.strongEpi_of_epi
theorem CategoryTheory.strongEpi_of_epi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} [inst_1 : CategoryTheory.StrongEpiCategory C]
(f : P ⟶ Q) [inst_2 : CategoryTheory.Epi f], CategoryTheory.StrongEpi f
This theorem states that in a category 'C' with objects 'P' and 'Q', and where 'C' is a Strong Epi Category, if a morphism 'f' from 'P' to 'Q' is an epimorphism, then 'f' is also a strong epimorphism. In category theory, an epimorphism is a morphism which is right-cancellative, and a strong epimorphism is a generalization of this concept.
More concisely: In a Strong Epi Category 'C', every epimorphism is a strong epimorphism.
|
CategoryTheory.isIso_of_mono_of_strongEpi
theorem CategoryTheory.isIso_of_mono_of_strongEpi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} (f : P ⟶ Q) [inst_1 : CategoryTheory.Mono f]
[inst_2 : CategoryTheory.StrongEpi f], CategoryTheory.IsIso f
This theorem states that in any category, if a morphism (or "arrow") is both a monomorphism (an injective function) and a strong epimorphism (a type of surjective function), then it is an isomorphism (a bijective function). This theorem applies for any objects `P` and `Q` in a category `C`.
More concisely: In any category, if a morphism is both a monomorphism and a strong epimorphism, then it is an isomorphism.
|
CategoryTheory.isIso_of_epi_of_strongMono
theorem CategoryTheory.isIso_of_epi_of_strongMono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} (f : P ⟶ Q) [inst_1 : CategoryTheory.Epi f]
[inst_2 : CategoryTheory.StrongMono f], CategoryTheory.IsIso f
This theorem states that in any category `C`, for any two objects `P` and `Q` in `C`, if morphism `f` from `P` to `Q` is an epimorphism and a strong monomorphism, then `f` is an isomorphism. In other words, if a morphism is both 'surjective' (epimorphism) and 'injective' in a strong sense (strong monomorphism), then it is an isomorphism (a bijective morphism or an invertible morphism) in the category theory context.
More concisely: In any category, if a morphism is both an epimorphism and a strong monomorphism, then it is an isomorphism.
|