Projective

📁 Source: Mathlib/RingTheory/LocalProperties/Projective.lean

Statistics

Metric	Count
Definitions	0
Theorems split_surjective_of_localization_maximal, finrank_of_isLocalizedModule_of_free, free_of_isLocalizedModule, lift_rank_of_isLocalizedModule_of_free, projective_of_isLocalizedModule, projective_of_localization_maximal, projective_of_localization_maximal'	7
Total	7

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
split_surjective_of_localization_maximal 📖	—	comp Localization.AtPrime CommRing.toCommSemiring Ideal.IsMaximal.isPrime' Localization CommSemiring.toCommMonoid Ideal.primeCompl CommSemiring.toSemiring LocalizedModule AddCommGroup.toAddCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe LinearMap addCommMonoid module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule instFunLike LocalizedModule.map id	—	—	Ideal.IsMaximal.isPrime' RingHomCompTriple.ids smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 Submodule.mem_of_localization_maximal instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation RingHomSurjective.ids instSMulCommClass LocalizedModule.map_id Function.Bijective.injective Module.End.isUnit_iff IsLocalizedModule.map_units Submonoid.smul_def map_smul_of_tower IsScalarTower.compatibleSMul instIsScalarTower IsLocalizedModule.mk'_cancel' restrictScalars_injective IsLocalizedModule.ext localizedModuleIsLocalizedModule ext IsLocalizedModule.mk'_surjective

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_of_isLocalizedModule_of_free 📖	mathematical	—	finrank CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	Cardinal.toNat_lift lift_rank_of_isLocalizedModule_of_free
free_of_isLocalizedModule 📖	mathematical	—	Free CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	Free.of_equiv Algebra.to_smulCommClass Free.tensor IsScalarTower.right Free.self IsLocalizedModule.isBaseChange
lift_rank_of_isLocalizedModule_of_free 📖	mathematical	—	Cardinal.lift rank CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	Cardinal.lift_injective RingHom.domain_nontrivial Algebra.to_smulCommClass LinearEquiv.lift_rank_eq IsLocalizedModule.isBaseChange Cardinal.lift_lift Cardinal.lift_umax IsScalarTower.to_smulCommClass IsScalarTower.right rank_tensorProduct commRing_strongRankCondition Free.self rank_self Cardinal.lift_one one_mul
projective_of_isLocalizedModule 📖	mathematical	—	Projective CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	Projective.of_equiv Algebra.to_smulCommClass Projective.tensorProduct IsScalarTower.right Projective.of_free Free.self IsLocalizedModule.isBaseChange
projective_of_localization_maximal 📖	—	Projective Localization.AtPrime CommRing.toCommSemiring Ideal.IsMaximal.isPrime' OreLocalization.instSemiring CommSemiring.toSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid LocalizedModule AddCommGroup.toAddCommMonoid OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction OreLocalization.instModule	—	—	Ideal.IsMaximal.isPrime' instFiniteOfFinitePresentation RingHomSurjective.ids LinearMap.range_eq_top Finsupp.range_linearCombination Subtype.range_val RingHomCompTriple.ids smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 projective_lifting_property LocalizedModule.map_surjective LinearMap.split_surjective_of_localization_maximal Projective.of_split Projective.of_free Free.finsupp Free.self
projective_of_localization_maximal' 📖	—	IsLocalization.AtPrime CommRing.toCommSemiring Ideal.IsMaximal.isPrime' IsScalarTower Algebra.toSMul CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction AddCommGroup.toAddCommMonoid IsLocalizedModule Ideal.primeCompl Projective	—	—	Ideal.IsMaximal.isPrime' projective_of_localization_maximal Projective.of_ringEquiv Localization.isLocalization RingHomInvPair.ids IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHomInvPair.of_ringEquiv IsLocalization.exists_mk'_eq smulCommClass_self End.isUnit_iff IsLocalizedModule.map_units SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass IsLocalization.smul_mk'_self algebraMap_smul IsLocalization.map_id_mk' OreLocalization.instIsScalarTower_1 LinearEquiv.left_inv LinearEquiv.right_inv

---

← Back to Index