Pseudoelements

📁 Source: Mathlib/CategoryTheory/Abelian/Pseudoelements.lean

Statistics

Metric	Count
Definitions PseudoEqual, hasZero, homToFun, instInhabited, objectToSort, overToSort, pseudoApply, pseudoZero, setoid, app	10
Theorems eq_range_of_pseudoequal, apply_eq_zero_of_comp_eq_zero, apply_zero, comp_apply, comp_comp, epi_of_pseudo_surjective, eq_zero_iff, exact_of_pseudo_exact, mono_of_zero_of_map_zero, over_coe_def, pseudoApply_aux, pseudoApply_mk', pseudoZero_aux, pseudoZero_def, pseudoZero_iff, pseudo_exact_of_exact, pseudo_injective_of_mono, pseudo_pullback, pseudo_surjective_of_epi, sub_of_eq_image, zero_apply, zero_eq_zero, zero_eq_zero', zero_morphism_ext, zero_morphism_ext', zero_of_map_zero, app_hom, pseudoEqual_refl, pseudoEqual_symm, pseudoEqual_trans	30
Total	40

CategoryTheory.Abelian

Definitions

Name	Category	Theorems
PseudoEqual 📖	MathDef	6 math math: Pseudoelement.pseudoZero_iff, pseudoEqual_refl, pseudoEqual_symm, pseudoEqual_trans, Pseudoelement.apply_eq_zero_of_comp_eq_zero, Pseudoelement.over_coe_def
app 📖	CompOp	2 math math: Pseudoelement.pseudoApply_aux, app_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit app CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right	—	—
pseudoEqual_refl 📖	mathematical	—	Reflexive CategoryTheory.Over PseudoEqual	—	CategoryTheory.instEpiId CategoryTheory.Category.id_comp
pseudoEqual_symm 📖	mathematical	—	Symmetric CategoryTheory.Over PseudoEqual	—	—
pseudoEqual_trans 📖	mathematical	—	Transitive CategoryTheory.Over PseudoEqual	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits hasFiniteLimits CategoryTheory.epi_comp epi_pullback_of_epi_g epi_pullback_of_epi_f CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.condition

CategoryTheory.Abelian.Pseudoelement

Definitions

Name	Category	Theorems
hasZero 📖	CompOp	8 math math: pseudoZero_def, apply_zero, pseudoZero_iff, sub_of_eq_image, zero_eq_zero, eq_zero_iff, apply_eq_zero_of_comp_eq_zero, zero_apply
homToFun 📖	CompOp	—
instInhabited 📖	CompOp	—
objectToSort 📖	CompOp	—
overToSort 📖	CompOp	—
pseudoApply 📖	CompOp	9 math math: apply_zero, comp_apply, pseudoApply_mk', pseudo_surjective_of_epi, comp_comp, eq_zero_iff, apply_eq_zero_of_comp_eq_zero, zero_apply, pseudo_injective_of_mono
pseudoZero 📖	CompOp	—
setoid 📖	CompOp	6 math math: pseudoZero_def, zero_eq_zero', pseudoApply_mk', zero_eq_zero, pseudoZero_aux, over_coe_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_zero_of_comp_eq_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	pseudoApply CategoryTheory.Over CategoryTheory.Abelian.PseudoEqual CategoryTheory.Abelian.Pseudoelement hasZero	—	zero_eq_zero
apply_zero 📖	mathematical	—	pseudoApply CategoryTheory.Abelian.Pseudoelement hasZero	—	pseudoZero_def pseudoApply_mk' CategoryTheory.Limits.zero_comp zero_eq_zero
comp_apply 📖	mathematical	—	pseudoApply CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.assoc CategoryTheory.Over.coe_hom
comp_comp 📖	mathematical	—	CategoryTheory.Abelian.Pseudoelement pseudoApply CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	comp_apply
epi_of_pseudo_surjective 📖	mathematical	CategoryTheory.Abelian.Pseudoelement pseudoApply	CategoryTheory.Epi	—	CategoryTheory.epi_of_epi_fac CategoryTheory.Category.assoc CategoryTheory.Category.comp_id
eq_zero_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive pseudoApply CategoryTheory.Abelian.Pseudoelement hasZero	—	zero_apply zero_morphism_ext
exact_of_pseudo_exact 📖	mathematical	pseudoApply CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	CategoryTheory.ShortComplex.Exact	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian apply_eq_zero_of_comp_eq_zero CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.Category.assoc CategoryTheory.Abelian.image.fac CategoryTheory.isIso_of_mono_of_epi CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.Limits.pullback.snd_of_mono CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.epi_of_epi_fac CategoryTheory.Iso.eq_inv_comp CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.HasZeroMorphisms.comp_zero
mono_of_zero_of_map_zero 📖	mathematical	CategoryTheory.Abelian.Pseudoelement hasZero	CategoryTheory.Mono	—	CategoryTheory.Preadditive.mono_iff_cancel_zero pseudoZero_iff
over_coe_def 📖	mathematical	—	CategoryTheory.Over CategoryTheory.Abelian.PseudoEqual setoid	—	—
pseudoApply_aux 📖	mathematical	CategoryTheory.Over setoid	CategoryTheory.Abelian.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
pseudoApply_mk' 📖	mathematical	—	pseudoApply CategoryTheory.Over setoid CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
pseudoZero_aux 📖	mathematical	—	CategoryTheory.Over setoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right	—	CategoryTheory.Limits.zero_of_epi_comp CategoryTheory.Limits.comp_zero CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Abelian.has_finite_products Finite.of_fintype CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsRegularEpi CategoryTheory.instIsRegularEpiOfIsSplitEpi CategoryTheory.Limits.biprod.fst_epi CategoryTheory.Limits.biprod.snd_epi CategoryTheory.Over.coe_hom CategoryTheory.Limits.HasZeroMorphisms.comp_zero
pseudoZero_def 📖	mathematical	—	CategoryTheory.Abelian.Pseudoelement hasZero CategoryTheory.Over setoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	—
pseudoZero_iff 📖	mathematical	—	CategoryTheory.Over CategoryTheory.Abelian.PseudoEqual CategoryTheory.Abelian.Pseudoelement hasZero CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	pseudoZero_aux Quotient.eq'
pseudo_exact_of_exact 📖	mathematical	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive pseudoApply CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.Abelian.Pseudoelement hasZero	CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f	—	pseudoZero_iff CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Abelian.image_ι_comp_eq_zero CategoryTheory.ShortComplex.zero CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.instEpiId CategoryTheory.Abelian.epi_pullback_of_epi_f CategoryTheory.Abelian.instEpiFactorThruImage CategoryTheory.Category.id_comp CategoryTheory.Abelian.image.fac CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.condition
pseudo_injective_of_mono 📖	mathematical	—	CategoryTheory.Abelian.Pseudoelement pseudoApply	—	CategoryTheory.cancel_mono CategoryTheory.Category.assoc
pseudo_pullback 📖	mathematical	pseudoApply	CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc CategoryTheory.instEpiId CategoryTheory.Category.id_comp
pseudo_surjective_of_epi 📖	mathematical	—	CategoryTheory.Abelian.Pseudoelement pseudoApply	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.instEpiId CategoryTheory.Abelian.epi_pullback_of_epi_f CategoryTheory.Category.id_comp CategoryTheory.Limits.pullback.condition CategoryTheory.Abelian.app_hom CategoryTheory.Over.coe_hom
sub_of_eq_image 📖	mathematical	pseudoApply	CategoryTheory.Abelian.Pseudoelement hasZero	—	CategoryTheory.Preadditive.sub_comp CategoryTheory.Category.assoc sub_eq_zero zero_eq_zero CategoryTheory.Preadditive.epi_iff_cancel_zero CategoryTheory.Limits.comp_zero CategoryTheory.instEpiId sub_eq_add_neg CategoryTheory.Preadditive.add_comp CategoryTheory.Preadditive.neg_comp neg_zero add_zero CategoryTheory.Category.id_comp
zero_apply 📖	mathematical	—	pseudoApply Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Abelian.Pseudoelement hasZero	—	pseudoZero_def pseudoApply_mk' CategoryTheory.Limits.comp_zero zero_eq_zero
zero_eq_zero 📖	mathematical	—	CategoryTheory.Over setoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Abelian.Pseudoelement hasZero	—	zero_eq_zero'
zero_eq_zero' 📖	mathematical	—	CategoryTheory.Over setoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	pseudoZero_aux
zero_morphism_ext 📖	mathematical	pseudoApply CategoryTheory.Abelian.Pseudoelement hasZero	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.id_comp pseudoZero_iff
zero_morphism_ext' 📖	mathematical	pseudoApply CategoryTheory.Abelian.Pseudoelement hasZero	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	zero_morphism_ext
zero_of_map_zero 📖	—	CategoryTheory.Abelian.Pseudoelement pseudoApply hasZero	—	—	apply_zero

CategoryTheory.Abelian.Pseudoelement.ModuleCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_range_of_pseudoequal 📖	mathematical	CategoryTheory.Abelian.PseudoEqual ModuleCat ModuleCat.moduleCategory	LinearMap.range ModuleCat.carrier CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom CategoryTheory.Comma.hom	—	RingHomSurjective.ids Submodule.ext ModuleCat.epi_iff_surjective RingHomCompTriple.ids LinearMap.comp_apply ModuleCat.hom_comp

---

← Back to Index