Linear

📁 Source: Mathlib/Algebra/Homology/DerivedCategory/Ext/Linear.lean

Statistics

Metric	Count
Definitions bilinearCompOfLinear, homLinearEquiv, instModule, linearEquiv₀, postcompOfLinear, precompOfLinear	6
Theorems bilinearCompOfLinear_apply_apply, comp_smul, homLinearEquiv_apply, homLinearEquiv_symm_apply, linearEquiv₀_symm_apply, mk₀_linearEquiv₀_apply, mk₀_smul, smul_comp, smul_eq_comp_mk₀, smul_hom	10
Total	16

CategoryTheory.Abelian.Ext

Definitions

Name	Category	Theorems
bilinearCompOfLinear 📖	CompOp	1 math math: bilinearCompOfLinear_apply_apply
homLinearEquiv 📖	CompOp	2 math math: homLinearEquiv_apply, homLinearEquiv_symm_apply
instModule 📖	CompOp	15 math math: CategoryTheory.Functor.mapExtLinearMap_toAddMonoidHom, homLinearEquiv_apply, smul_hom, mk₀_smul, CategoryTheory.Functor.mapExtLinearMap_coe, smul_comp, CategoryTheory.Functor.mapExactFunctor_smul, comp_smul, bilinearCompOfLinear_apply_apply, smul_eq_comp_mk₀, ModuleCat.finite_ext, mk₀_linearEquiv₀_apply, linearEquiv₀_symm_apply, homLinearEquiv_symm_apply, CategoryTheory.Functor.mapExtLinearMap_apply
linearEquiv₀ 📖	CompOp	2 math math: mk₀_linearEquiv₀_apply, linearEquiv₀_symm_apply
postcompOfLinear 📖	CompOp	—
precompOfLinear 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bilinearCompOfLinear_apply_apply 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CategoryTheory.Abelian.Ext AddCommGroup.toAddCommMonoid instAddCommGroup instModule CommRing.toRing LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring bilinearCompOfLinear comp	—	CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor smulCommClass_self
comp_smul 📖	mathematical	CategoryTheory.HasExt	comp CategoryTheory.Abelian.Ext SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModule	—	ext comp_hom CategoryTheory.ShiftedHom.comp.congr_simp smul_hom CategoryTheory.ShiftedHom.comp_smul DerivedCategory.instLinearShiftFunctorInt
homLinearEquiv_apply 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids CategoryTheory.Abelian.Ext CategoryTheory.ShiftedHom DerivedCategory DerivedCategory.instCategory Int.instAddMonoid DerivedCategory.instHasShiftInt CategoryTheory.Functor.obj DerivedCategory.singleFunctor AddCommGroup.toAddCommMonoid instAddCommGroup CategoryTheory.Preadditive.homGroup DerivedCategory.instPreadditive CategoryTheory.shiftFunctor instModule CategoryTheory.Linear.homModule DerivedCategory.instLinear EquivLike.toFunLike LinearEquiv.instEquivLike homLinearEquiv Equiv.toFun AddEquiv.toEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup homAddEquiv	—	RingHomInvPair.ids
homLinearEquiv_symm_apply 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids CategoryTheory.ShiftedHom DerivedCategory DerivedCategory.instCategory Int.instAddMonoid DerivedCategory.instHasShiftInt CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.Abelian.Ext AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup DerivedCategory.instPreadditive CategoryTheory.shiftFunctor instAddCommGroup CategoryTheory.Linear.homModule DerivedCategory.instLinear instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm homLinearEquiv Equiv.invFun AddEquiv.toEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup homAddEquiv	—	CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor RingHomInvPair.ids
linearEquiv₀_symm_apply 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.Ext AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Abelian.toPreadditive instAddCommGroup CategoryTheory.Linear.homModule instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm linearEquiv₀ mk₀	—	CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasZeroObject CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor RingHomInvPair.ids
mk₀_linearEquiv₀_apply 📖	mathematical	CategoryTheory.HasExt	mk₀ DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids CategoryTheory.Abelian.Ext Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommGroup.toAddCommMonoid instAddCommGroup CategoryTheory.Preadditive.homGroup CategoryTheory.Abelian.toPreadditive instModule CategoryTheory.Linear.homModule EquivLike.toFunLike LinearEquiv.instEquivLike linearEquiv₀	—	Equiv.left_inv
mk₀_smul 📖	mathematical	CategoryTheory.HasExt	mk₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.Abelian.toPreadditive DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid CategoryTheory.Linear.homModule CategoryTheory.Abelian.Ext instAddCommGroup instModule	—	ext mk₀_hom CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Functor.map_smul DerivedCategory.instLinearSingleFunctor CategoryTheory.ShiftedHom.mk₀_smul smul_hom
smul_comp 📖	mathematical	CategoryTheory.HasExt	comp CategoryTheory.Abelian.Ext SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModule	—	ext comp_hom CategoryTheory.ShiftedHom.comp.congr_simp smul_hom CategoryTheory.ShiftedHom.smul_comp
smul_eq_comp_mk₀ 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Abelian.Ext SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModule comp mk₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Preadditive.homGroup CategoryTheory.Abelian.toPreadditive CategoryTheory.Linear.homModule CategoryTheory.CategoryStruct.id add_zero Nat.instAddMonoid	—	ext add_zero RingHomInvPair.ids LinearEquiv.map_smul comp_hom mk₀_hom CategoryTheory.Functor.map_smul DerivedCategory.instLinearSingleFunctor CategoryTheory.Functor.map_id CategoryTheory.ShiftedHom.mk₀_smul CategoryTheory.ShiftedHom.comp_smul DerivedCategory.instLinearShiftFunctorInt CategoryTheory.ShiftedHom.comp_mk₀_id
smul_hom 📖	mathematical	CategoryTheory.HasExt	hom CategoryTheory.Abelian.Ext SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModule CategoryTheory.ShiftedHom DerivedCategory DerivedCategory.instCategory Int.instAddMonoid DerivedCategory.instHasShiftInt CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.Preadditive.homGroup DerivedCategory.instPreadditive CategoryTheory.shiftFunctor CategoryTheory.Linear.homModule DerivedCategory.instLinear	—	add_zero smul_eq_comp_mk₀ comp_hom CategoryTheory.ShiftedHom.comp.congr_simp mk₀_hom CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Functor.map_smul DerivedCategory.instLinearSingleFunctor CategoryTheory.Functor.map_id CategoryTheory.ShiftedHom.mk₀_smul CategoryTheory.ShiftedHom.comp_smul DerivedCategory.instLinearShiftFunctorInt CategoryTheory.ShiftedHom.comp_mk₀_id

---

← Back to Index