Linear

📁 Source: Mathlib/CategoryTheory/Localization/Linear.lean

Statistics

Metric	Count
Definitions instLinearLocalization, instLinearLocalization', linear	3
Theorems functor_linear, functor_linear_iff, instLinearLocalization'Q', instLinearLocalizationQ	4
Total	7

CategoryTheory.Localization

Definitions

Name	Category	Theorems
instLinearLocalization 📖	CompOp	1 math math: instLinearLocalizationQ
instLinearLocalization' 📖	CompOp	1 math math: instLinearLocalization'Q'
linear 📖	CompOp	1 math math: functor_linear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functor_linear 📖	mathematical	—	CategoryTheory.Functor.Linear Ring.toSemiring linear	—	CategoryTheory.CatCenter.localization_app CategoryTheory.Functor.map_comp CategoryTheory.Linear.smul_comp CategoryTheory.Category.id_comp
functor_linear_iff 📖	mathematical	—	CategoryTheory.Functor.Linear Ring.toSemiring	—	CategoryTheory.Functor.linear_of_iso essSurj CategoryTheory.Functor.linear_iff CategoryTheory.Linear.smul_comp CategoryTheory.Category.id_comp CategoryTheory.Linear.comp_smul CategoryTheory.Iso.inv_hom_id CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_id CategoryTheory.Functor.map_smul CategoryTheory.Functor.comp_map CategoryTheory.Functor.instLinearComp
instLinearLocalization'Q' 📖	mathematical	—	CategoryTheory.Functor.Linear Ring.toSemiring CategoryTheory.MorphismProperty.Localization' CategoryTheory.MorphismProperty.instCategoryLocalization' instLinearLocalization' CategoryTheory.MorphismProperty.Q'	—	functor_linear CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q'
instLinearLocalizationQ 📖	mathematical	—	CategoryTheory.Functor.Linear Ring.toSemiring CategoryTheory.MorphismProperty.Localization CategoryTheory.MorphismProperty.instCategoryLocalization instLinearLocalization CategoryTheory.MorphismProperty.Q	—	functor_linear CategoryTheory.Functor.q_isLocalization

---

← Back to Index