Instances

📁 Source: Mathlib/Algebra/Category/Ring/Instances.lean

Statistics

Metric	Count
Definitions	0
Theorems isLocalHom_comp, epi, epi, epi', isLocalHom_of_isIso, isLocalHom_of_iso, localization_unit_isIso, localization_unit_isIso'	8
Total	8

CommRingCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalHom_comp 📖	mathematical	—	IsLocalHom carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike Hom.hom CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct instCategory	—	RingHom.isLocalHom_comp

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi 📖	mathematical	—	CategoryTheory.Epi CommRingCat CommRingCat.instCategory CommRingCat.of CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring	—	CommRingCat.hom_ext ringHom_ext

Localization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi 📖	mathematical	—	CategoryTheory.Epi CommRingCat CommRingCat.instCategory CommRingCat.of Localization CommRing.toCommMonoid OreLocalization.instCommRing OreLocalization.oreSetComm CommRingCat.ofHom algebraMap CommRing.toCommSemiring OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.instAlgebra Algebra.id	—	IsLocalization.epi isLocalization
epi' 📖	mathematical	—	CategoryTheory.Epi CommRingCat CommRingCat.instCategory CommRingCat.of Localization CommRingCat.carrier CommRing.toCommMonoid CommRingCat.commRing OreLocalization.instCommRing OreLocalization.oreSetComm CommRingCat.ofHom algebraMap CommRing.toCommSemiring OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.instAlgebra Algebra.id	—	IsLocalization.epi isLocalization

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalHom_of_isIso 📖	mathematical	—	IsLocalHom CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom	—	isLocalHom_of_iso
isLocalHom_of_iso 📖	mathematical	—	IsLocalHom CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Iso.hom CommRingCat CommRingCat.instCategory	—	CategoryTheory.Iso.hom_inv_id_apply RingHom.isUnit_map
localization_unit_isIso 📖	mathematical	—	CategoryTheory.IsIso CommRingCat CommRingCat.instCategory CommRingCat.of CommRingCat.carrier CommRingCat.commRing Localization.Away CommRing.toCommMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm CommRingCat.ofHom algebraMap CommRing.toCommSemiring OreLocalization.instSemiring Ring.toSemiring OreLocalization.instAlgebra Algebra.id	—	CategoryTheory.Iso.isIso_hom Localization.isLocalization
localization_unit_isIso' 📖	mathematical	—	CategoryTheory.IsIso CommRingCat CommRingCat.instCategory CommRingCat.of Localization.Away CommRingCat.carrier CommRing.toCommMonoid CommRingCat.commRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm CommRingCat.ofHom algebraMap CommRing.toCommSemiring OreLocalization.instSemiring Ring.toSemiring OreLocalization.instAlgebra Algebra.id	—	localization_unit_isIso

---

← Back to Index