Composition of effective epimorphisms

This file provides EffectiveEpi instances for certain compositions.

noncomputable def CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} {Y : C} (f : X ⟶ B) (g : Y ⟶ X) (i : X ⟶ Y) (hi : CategoryTheory.CategoryStruct.comp i g = CategoryTheory.CategoryStruct.id X) [CategoryTheory.EffectiveEpi f] : CategoryTheory.EffectiveEpiStruct (CategoryTheory.CategoryStruct.comp g f)

A split epi followed by an effective epi is an effective epi. This version takes an explicit section to the split epi, and is mainly used to define effectiveEpiStructCompOfEffectiveEpiSplitEpi, which takes a IsSplitEpi instance instead.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} {Y : C} (f : X ⟶ B) (g : Y ⟶ X) [CategoryTheory.IsSplitEpi g] [CategoryTheory.EffectiveEpi f] : CategoryTheory.EffectiveEpiStruct (CategoryTheory.CategoryStruct.comp g f)

A split epi followed by an effective epi is an effective epi.

Equations

• CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi f g = CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi' f g (Nonempty.some ⋯).section_ ⋯

instance CategoryTheory.instEffectiveEpiCompToCategoryStruct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} {Y : C} (f : X ⟶ B) (g : Y ⟶ X) [CategoryTheory.IsSplitEpi g] [CategoryTheory.EffectiveEpi f] : CategoryTheory.EffectiveEpi (CategoryTheory.CategoryStruct.comp g f)

Equations

• ⋯ = ⋯

theorem CategoryTheory.effectiveEpiFamilyStructCompIso_aux {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {B' : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) (i : B ⟶ B') {W : C} (e : (a : α) → X a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.comp (π a₁) i) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.CategoryStruct.comp (π a₂) i) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) {Z : C} (a₁ : α) (a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂) (hg : CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂)) : CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)

noncomputable def CategoryTheory.effectiveEpiFamilyStructCompIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {B' : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (i : B ⟶ B') [CategoryTheory.IsIso i] : CategoryTheory.EffectiveEpiFamilyStruct X fun (a : α) => CategoryTheory.CategoryStruct.comp (π a) i

An effective epi family followed by an iso is an effective epi family.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.instEffectiveEpiFamilyCompToCategoryStruct {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {B' : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (i : B ⟶ B') [CategoryTheory.IsIso i] : CategoryTheory.EffectiveEpiFamily X fun (a : α) => CategoryTheory.CategoryStruct.comp (π a) i

Equations

• ⋯ = ⋯

theorem CategoryTheory.effectiveEpiFamilyStructIsoComp_aux {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (Y : α → C) (π : (a : α) → X a ⟶ B) (i : (a : α) → Y a ⟶ X a) [∀ (a : α), CategoryTheory.IsIso (i a)] {W : C} (e : (a : α) → Y a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.comp (i a₁) (π a₁)) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.CategoryStruct.comp (i a₂) (π a₂)) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) {Z : C} (a₁ : α) (a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂) (hg : CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂)) : CategoryTheory.CategoryStruct.comp g₁ ((fun (a : α) => CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (i a)) (e a)) a₁) = CategoryTheory.CategoryStruct.comp g₂ ((fun (a : α) => CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (i a)) (e a)) a₂)

noncomputable def CategoryTheory.effectiveEpiFamilyStructIsoComp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (Y : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (i : (a : α) → Y a ⟶ X a) [∀ (a : α), CategoryTheory.IsIso (i a)] : CategoryTheory.EffectiveEpiFamilyStruct Y fun (a : α) => CategoryTheory.CategoryStruct.comp (i a) (π a)

An effective epi family preceded by a family of isos is an effective epi family.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.effectiveEpiFamilyIsoComp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (Y : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (i : (a : α) → Y a ⟶ X a) [∀ (a : α), CategoryTheory.IsIso (i a)] : CategoryTheory.EffectiveEpiFamily Y fun (a : α) => CategoryTheory.CategoryStruct.comp (i a) (π a)

Equations

• ⋯ = ⋯