FinitePresentation

📁 Source: Mathlib/Algebra/Module/FinitePresentation.lean

Statistics

Metric	Count
Definitions FinitePresentation, FinitePresentation, linearEquivMap, linearEquivMapExtendScalars	4
Theorems of_isBaseChange, exists_isLocalizedModule_powers_of_finitePresentation, finitePresentation_iff, exists_smul_of_comp_eq_of_isLocalizedModule, equiv_quotient, exists_fin, exists_lift_equiv_of_isLocalizedModule, exists_lift_of_isLocalizedModule, exists_notMem_bijective, fg_ker, fg_ker_iff, isLocalizedModule_map, isLocalizedModule_mapExtendScalars, linearEquivMapExtendScalars_apply, linearEquivMapExtendScalars_symm_apply, linearEquivMap_apply, linearEquivMap_symm_apply, of_equiv, of_subsingleton, out, pi, prod, trans, finitePresentation_iff_finite, finitePresentation_of_finite, finitePresentation_of_free_of_surjective, finitePresentation_of_ker, finitePresentation_of_projective, finitePresentation_of_projective_of_exact, finitePresentation_of_split_exact, finitePresentation_of_surjective, exists_bijective_map_powers, instFiniteOfFinitePresentation, instFinitePresentation, instFinitePresentationFinsupp, instFinitePresentationForall, instFinitePresentationLocalizationLocalizedModule, instFinitePresentationTensorProduct, instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation	39
Total	43

Algebra

Definitions

Name	Category	Theorems
FinitePresentation 📖	CompData	29 math math: FinitePresentation.equiv, Polynomial.instFinitePresentationUniversalFactorizationRing, smooth_iff, FinitePresentation.mvPolynomial_of_finitePresentation, instFinitePresentationAway, IsLocalization.Away.finitePresentation, Smooth.finitePresentation, FinitePresentation.mvPolynomial, FinitePresentation.iff, Module.FinitePresentation.iff_finitePresentation_of_finite, FinitePresentation.of_restrict_scalars_finitePresentation, FinitePresentation.of_surjective, FinitePresentation.self, Presentation.instFinitePresentationModelOfHasCoeffsOfFinite, Presentation.finitePresentation_of_isFinite, FinitePresentation.of_finiteType, RingHom.finitePresentation_algebraMap, AdjoinRoot.finitePresentation, FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlat, FinitePresentation.polynomial, Etale.finitePresentation, FinitePresentation.of_finitePresentation, IsStandardSmooth.finitePresentation, FinitePresentation.baseChange, Presentation.instFinitePresentationQuotientOfFinite, FinitePresentation.trans, FinitePresentation.quotient, FinitePresentation.of_isLocalizationAway, FinitePresentation.iff_quotient_mvPolynomial'

FinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isBaseChange 📖	mathematical	IsBaseChange AddCommGroup.toAddCommMonoid CommRing.toCommSemiring	Module.FinitePresentation CommSemiring.toSemiring	—	Module.finitePresentation_of_surjective Algebra.to_smulCommClass instFinitePresentationTensorProduct RingHomInvPair.ids LinearEquiv.surjective LinearEquiv.ker Submodule.fg_bot

IsLocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isLocalizedModule_powers_of_finitePresentation 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike IsLocalizedModule AddCommGroup.toAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	map_units one_smul Zero.instNonempty Submonoid.one_mem smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 exists_bijective_map_powers ext RingHomCompTriple.ids map_comp Function.bijective_id dvd_rfl localizedModuleIsLocalizedModule mk'_surjective pow_add SemigroupAction.mul_smul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass map_mk' mk_eq_mk' exists_of_eq

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finitePresentation_iff 📖	mathematical	—	Module.FinitePresentation Ring.toSemiring AddCommGroup.toAddCommMonoid	—	RingHomInvPair.ids Module.FinitePresentation.of_equiv

Module

Definitions

Name	Category	Theorems
FinitePresentation 📖	CompData	26 math math: finitePresentation_of_ker, finitePresentation_of_free_of_surjective, Algebra.FormallySmooth.instFinitePresentationKaehlerDifferentialOfEssFiniteType, FinitePresentation.prod, LinearEquiv.finitePresentation_iff, instFinitePresentationFinsupp, FinitePresentation.trans, instFinitePresentationForall, finitePresentation_of_surjective, FinitePresentation.of_equiv, instFinitePresentationLocalizationLocalizedModule, finitePresentation_of_projective_of_exact, FinitePresentation.iff_finitePresentation_of_finite, finitePresentation_of_split_exact, FinitePresentation.of_subsingleton, instFinitePresentation, finitePresentation_of_projective, FinitePresentation.fg_ker_iff, finitePresentation_of_finite, finitePresentation_iff_exists_presentation, finitePresentation_iff_finite, FinitePresentation.of_isBaseChange, Presentation.finitePresentation, Algebra.instFinitePresentationKaehlerDifferentialOfFinitePresentation, FinitePresentation.of_finite_of_finitePresentation, instFinitePresentationTensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finitePresentation_iff_finite 📖	mathematical	—	FinitePresentation Ring.toSemiring AddCommGroup.toAddCommMonoid Finite	—	instFiniteOfFinitePresentation finitePresentation_of_finite
finitePresentation_of_finite 📖	mathematical	—	FinitePresentation Ring.toSemiring AddCommGroup.toAddCommMonoid	—	IsNoetherian.noetherian isNoetherian_of_isNoetherianRing_of_finite Finite.finsupp Finite.of_fintype Finite.self
finitePresentation_of_free_of_surjective 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike Submodule.FG LinearMap.ker	FinitePresentation	—	Set.finite_range Finite.of_fintype Set.toFinite Set.toFinite_toFinset Set.toFinset_range RingHomSurjective.ids Set.range_comp Set.Finite.toFinset.congr_simp Set.toFinset_image Finset.coe_image Finset.coe_univ Set.image_univ Submodule.span_image Submodule.map.congr_simp Basis.span_eq Submodule.map_top RingHomCompTriple.ids RingHomInvPair.ids Submodule.ext Basis.repr_symm_apply Finsupp.linearCombination_mapDomain Finsupp.apply_linearCombination LinearEquiv.apply_symm_apply Finsupp.mapDomain_comp Finsupp.mapDomain_id Basis.linearCombination_repr Submodule.FG.map
finitePresentation_of_ker 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	FinitePresentation	—	Submodule.fg_of_fg_map_of_fg_inf_ker RingHomSurjective.ids Submodule.map_top LinearMap.range_eq_top Finite.fg_top instFiniteOfFinitePresentation top_inf_eq Finite.iff_fg Finsupp.range_linearCombination Subtype.range_val RingHomCompTriple.ids Finite.of_fg FinitePresentation.fg_ker Finite.finsupp Finite.of_fintype Finite.self LinearMap.ext Submodule.map_injective_of_injective Submodule.injective_subtype Submodule.range_subtype LinearMap.range_comp LinearMap.ker_comp Submodule.map_comap_eq_of_surjective Submodule.comap_mono bot_le inf_eq_right Submodule.map_comap_eq LinearMap.ker_eq_bot Submodule.comap_bot Submodule.FG.map
finitePresentation_of_projective 📖	mathematical	—	FinitePresentation Ring.toSemiring AddCommGroup.toAddCommMonoid	—	RingHomCompTriple.ids Finite.exists_comp_eq_id_of_projective finitePresentation_of_free_of_surjective Free.function Finite.of_fintype Free.self Finite.pi Finite.self RingHomSurjective.ids Submodule.FG.of_finite Finite.range LinearMap.ker_eq_range_of_comp_eq_id
finitePresentation_of_projective_of_exact 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike Function.Exact NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	FinitePresentation	—	RingHomCompTriple.ids projective_lifting_property finitePresentation_of_split_exact
finitePresentation_of_split_exact 📖	mathematical	LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.id DFunLike.coe LinearMap LinearMap.instFunLike Function.Exact NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	FinitePresentation	—	RingHomCompTriple.ids Function.LeftInverse.surjective DFunLike.congr_fun Finite.of_surjective RingHomSurjective.ids instFiniteOfFinitePresentation RingHomInvPair.ids List.TFAE.out Function.Exact.split_tfae' finitePresentation_of_surjective Prod.fst_surjective Zero.instNonempty LinearEquiv.surjective LinearMap.ker_comp RingHomSurjective.invPair Submodule.comap_equiv_eq_map_symm LinearMap.exact_iff Function.Exact.inr_fst LinearMap.range_comp Submodule.fg_range
finitePresentation_of_surjective 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike Submodule.FG LinearMap.ker	FinitePresentation	—	RingHomSurjective.ids LinearMap.range_eq_top Finsupp.range_linearCombination Subtype.range_val finitePresentation_of_free_of_surjective Free.finsupp Free.self Finite.finsupp Finite.of_fintype Finite.self RingHomCompTriple.ids Set.image_image Set.image_congr Set.image_id' LinearMap.ker_comp Submodule.map_span Submodule.comap_map_eq Finset.coe_image Submodule.FG.sup

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_smul_of_comp_eq_of_isLocalizedModule 📖	mathematical	LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike LinearMap Submonoid.smul LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing	—	RingHomCompTriple.ids IsLocalizedModule.exists_of_eq LinearMap.congr_fun smulCommClass_self sub_eq_zero LinearMap.ker_eq_top top_le_iff Submodule.span_le SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass Finset.prod_erase_mul SemigroupAction.mul_smul

Module.FinitePresentation

Definitions

Name	Category	Theorems
linearEquivMap 📖	CompOp	2 math math: linearEquivMap_symm_apply, linearEquivMap_apply
linearEquivMapExtendScalars 📖	CompOp	2 math math: linearEquivMapExtendScalars_apply, linearEquivMapExtendScalars_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_quotient 📖	mathematical	—	Module.Free Ring.toSemiring AddCommGroup.toAddCommMonoid Module.Finite Submodule.FG	—	RingHomInvPair.ids exists_fin small_Pi UnivLE.small univLE_of_max UnivLE.self RingHomSurjective.ids RingHomCompTriple.ids Module.Free.of_equiv Module.Free.function Finite.of_fintype Module.Free.self Module.Finite.equiv Module.Finite.pi Module.Finite.self Submodule.FG.map
exists_fin 📖	mathematical	—	Submodule.FG Ring.toSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Pi.Function.module Semiring.toModule	—	RingHomInvPair.ids RingHomCompTriple.ids Finite.of_fintype RingHomSurjective.ids LinearMap.range_eq_top LinearMap.range.congr_simp LinearMap.comp.congr_simp LinearEquiv.trans.congr_simp Finsupp.lcongr_symm LinearEquiv.range_comp Finsupp.range_linearCombination Subtype.range_coe_subtype RingHomSurjective.invPair Submodule.comap_equiv_eq_map_symm Submodule.map.congr_simp Submodule.FG.map
exists_lift_equiv_of_isLocalizedModule 📖	mathematical	—	LinearMap.comp LocalizedModule CommRing.toCommSemiring Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring AddCommGroup.toAddCommMonoid OreLocalization.instAddCommMonoidOreLocalization OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LocalizedModule.lift IsLocalizedModule.map_units Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Monoid.toMulOneClass Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder SetLike.le_def instIsConcreteLE Submonoid.powers_le LinearMap.restrictScalars Localization CommRing.toCommMonoid CommMonoid.toMonoid OreLocalization.instSemiring Ring.toSemiring CommRing.toRing OreLocalization.instModule LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul OreLocalization.instSMulOfIsScalarTower Monoid.toMulAction Algebra.toSMul OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction LinearEquiv.toLinearMap RingHomInvPair.ids	—	RingHomInvPair.ids RingHomCompTriple.ids smulCommClass_self IsScalarTower.left IsScalarTower.right IsLocalizedModule.map_units SetLike.le_def instIsConcreteLE Submonoid.powers_le LinearMap.IsScalarTower.compatibleSMul OreLocalization.instIsScalarTower_1 exists_lift_of_isLocalizedModule IsLocalizedModule.ext LinearMap.ext IsLocalizedModule.map_apply LinearMap.comp_apply Function.Bijective.comp Module.End.isUnit_iff LinearEquiv.bijective IsScalarTower.to_smulCommClass' exists_bijective_map_powers instFiniteOfFinitePresentation isUnit_of_dvd_unit map_dvd NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_comm IsLocalization.map_units Localization.isLocalization Submonoid.mem_powers localizedModuleIsLocalizedModule IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Units.isUnit dvd_mul_right MulMemClass.mul_mem SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass LinearMap.congr_fun map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass smul_assoc Algebra.smul_def IsUnit.mul_val_inv one_smul map_one MonoidHomClass.toOneHomClass IsUnit.unit.congr_simp IsUnit.unit_one inv_one
exists_lift_of_isLocalizedModule 📖	mathematical	—	LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike LinearMap Submonoid.smul LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing	—	RingHomCompTriple.ids smulCommClass_self RingHomSurjective.ids LinearMap.range_eq_top Finsupp.range_linearCombination Subtype.range_val Finsupp.lhom_ext' LinearMap.ext_ring Finsupp.linearCombination_single one_smul LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul Submonoid.isScalarTower IsScalarTower.left SemigroupAction.mul_smul Finset.prod_erase_mul Subtype.prop smul_zero IsLocalizedModule.exists_of_eq LinearMap.comp_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.mem_ker Submodule.subset_span Submodule.span_le SetLike.mem_coe Submonoid.smulCommClass_right LinearMap.smul_apply Finset.mem_univ SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass RingHomInvPair.ids LinearMap.ext LinearMap.smul_comp LinearMap.comp_smul LinearMap.comp_assoc LinearMap.quotKerEquivOfSurjective_symm_apply IsLocalizedModule.surj
exists_notMem_bijective 📖	mathematical	Function.Bijective DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map Ideal.primeCompl	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Localization OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization OreLocalization.instModule OreLocalization.instModuleOfIsScalarTower IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Algebra.toModule LocalizedModule.map	—	smulCommClass_self IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 exists_bijective_map_powers dvd_rfl
fg_ker 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	Submodule.FG LinearMap.ker	—	RingHomSurjective.ids LinearMap.range_eq_top Finsupp.range_linearCombination Subtype.range_val RingHomCompTriple.ids Finsupp.lhom_ext' LinearMap.ext_ring Finsupp.linearCombination_single one_smul top_le_iff Submodule.mkQ_surjective map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sub_eq_zero LinearMap.comp_apply Submodule.fg_of_fg_map_of_fg_inf_ker Module.Finite.fg_top Module.Finite.quotient Submodule.ker_mkQ inf_comm Submodule.map_comap_eq LinearMap.ker_comp Submodule.FG.map
fg_ker_iff 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	Submodule.FG LinearMap.ker Module.FinitePresentation	—	Module.finitePresentation_of_surjective fg_ker instFiniteOfFinitePresentation
isLocalizedModule_map 📖	mathematical	—	IsLocalizedModule CommRing.toCommSemiring LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map	—	smulCommClass_self IsScalarTower.left Module.End.isUnit_iff IsLocalizedModule.map_units LinearMap.ext LinearMap.congr_fun RingHomCompTriple.ids Module.End.isUnit_apply_inv_apply_of_isUnit exists_lift_of_isLocalizedModule IsLocalizedModule.ext IsLocalizedModule.map_apply Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule instFiniteOfFinitePresentation
isLocalizedModule_mapExtendScalars 📖	mathematical	—	IsLocalizedModule CommRing.toCommSemiring LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' IsLocalizedModule.mapExtendScalars	—	IsLocalizedModule.of_linearEquiv smulCommClass_self IsScalarTower.to_smulCommClass' isLocalizedModule_map
linearEquivMapExtendScalars_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LocalizedModule LinearMap AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Localization OreLocalization.instCommSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toCommMonoid OreLocalization.instModule LinearMap.instDistribMulAction OreLocalization.instSemiring OreLocalization.instModuleOfIsScalarTower Semiring.toModule LinearMap.instIsScalarTower DistribMulAction.toDistribSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsScalarTower.left IsScalarTower.right Algebra.id IsScalarTower.to_smulCommClass' OreLocalization.instAlgebra OreLocalization.instIsScalarTower_1 SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Algebra.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv linearEquivMapExtendScalars LinearMap.instFunLike LocalizedModule.mkLinearMap IsLocalizedModule.mapExtendScalars localizedModuleIsLocalizedModule Localization.isLocalization	—	IsLocalizedModule.linearEquiv_apply smulCommClass_self
linearEquivMapExtendScalars_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Localization CommRing.toCommMonoid OreLocalization.instCommSemiring OreLocalization.oreSetComm LocalizedModule AddCommGroup.toAddCommMonoid OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing OreLocalization.instSemiring LinearMap.instDistribMulAction 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 LinearMap.instIsScalarTower DistribMulAction.toDistribSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm linearEquivMapExtendScalars LinearMap.instFunLike IsLocalizedModule.mapExtendScalars LocalizedModule.mkLinearMap localizedModuleIsLocalizedModule Localization.isLocalization	—	IsLocalizedModule.linearEquiv_symm_apply smulCommClass_self LinearMap.instIsScalarTower IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1
linearEquivMap_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LocalizedModule LinearMap AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left IsScalarTower.right Algebra.id LinearMap.instDistribMulAction LinearMap.instIsScalarTower DistribMulAction.toDistribSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv linearEquivMap LinearMap.instFunLike LocalizedModule.mkLinearMap IsLocalizedModule.map localizedModuleIsLocalizedModule	—	IsLocalizedModule.linearEquiv_apply smulCommClass_self IsScalarTower.left IsScalarTower.right
linearEquivMap_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap LocalizedModule AddCommGroup.toAddCommMonoid OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction CommRing.toCommMonoid OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommMonoid.toMonoid Ring.toSemiring CommRing.toRing LinearMap.instDistribMulAction LinearMap.instIsScalarTower DistribMulAction.toDistribSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm linearEquivMap LinearMap.instFunLike IsLocalizedModule.map LocalizedModule.mkLinearMap localizedModuleIsLocalizedModule	—	IsLocalizedModule.linearEquiv_symm_apply smulCommClass_self IsScalarTower.left IsScalarTower.right LinearMap.instIsScalarTower
of_equiv 📖	mathematical	—	Module.FinitePresentation Ring.toSemiring AddCommGroup.toAddCommMonoid	—	RingHomInvPair.ids fg_ker_iff LinearEquiv.surjective LinearEquiv.ker
of_subsingleton 📖	mathematical	—	Module.FinitePresentation Ring.toSemiring AddCommGroup.toAddCommMonoid	—	of_equiv RingHomInvPair.ids Unique.instSubsingleton Fin.isEmpty' instFinitePresentationForall Finite.of_fintype
out 📖	mathematical	—	Submodule.span SetLike.coe Finset Finset.instSetLike Top.top Submodule Submodule.instTop Submodule.FG Finsupp SetLike.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.ker RingHom.id Finsupp.linearCombination	—	—
pi 📖	mathematical	Module.FinitePresentation Ring.toSemiring AddCommGroup.toAddCommMonoid	Pi.addCommMonoid Pi.module	—	Module.pi_induction' RingHomInvPair.ids of_equiv of_subsingleton prod
prod 📖	mathematical	—	Module.FinitePresentation Ring.toSemiring Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid Prod.instModule	—	LinearMap.fst_surjective RingHomSurjective.ids LinearMap.ker_fst of_equiv RingHomInvPair.ids LinearMap.inr_injective Module.finitePresentation_of_ker
trans 📖	mathematical	—	Module.FinitePresentation CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	RingHomInvPair.ids exists_fin LinearMap.IsScalarTower.compatibleSMul Pi.isScalarTower IsScalarTower.right RingHomCompTriple.ids Module.finitePresentation_of_surjective pi Finite.of_fintype Submodule.mkQ_surjective LinearEquiv.symm_apply_apply Module.Finite.of_fg LinearEquiv.ker_comp Submodule.ker_mkQ Module.Finite.trans Submodule.restrictScalars.isScalarTower instFiniteOfFinitePresentation

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_bijective_map_powers 📖	mathematical	Function.Bijective DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsLocalizedModule.map	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike LocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Localization OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization OreLocalization.instModule 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 LocalizedModule.map	—	smulCommClass_self RingHomInvPair.ids RingHomCompTriple.ids IsScalarTower.left IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 Module.FinitePresentation.exists_lift_of_isLocalizedModule LinearMap.ext LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul Submonoid.isScalarTower IsLocalizedModule.map_apply LinearEquiv.apply_ofBijective_symm_apply Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule instFiniteOfFinitePresentation LinearMap.comp_assoc Submonoid.smulCommClass_right LinearMap.smul_comp IsLocalizedModule.map_comp LinearMap.comp.congr_simp LinearEquiv.self_trans_symm LinearMap.comp_smul Submonoid.mem_powers IsLocalization.map_units Localization.isLocalization isUnit_of_dvd_unit map_dvd NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass dvd_trans mul_assoc Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul LinearMap.instSMulCommClass LinearMap.instIsScalarTower Module.End.isUnit_iff IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass algebraMap_smul smul_assoc Algebra.smul_def IsUnit.mul_val_inv one_smul LinearMap.restrictScalars_injective IsLocalizedModule.ext localizedModuleIsLocalizedModule IsLocalizedModule.map_units OreLocalization.instSMulCommClass Algebra.to_smulCommClass LinearEquiv.bijective
instFiniteOfFinitePresentation 📖	mathematical	—	Module.Finite	—	—
instFinitePresentation 📖	mathematical	—	Module.FinitePresentation Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semiring.toModule	—	Module.finitePresentation_of_projective Module.Projective.of_free Module.Free.self Module.Finite.self
instFinitePresentationFinsupp 📖	mathematical	—	Module.FinitePresentation Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Ring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule	—	Module.finitePresentation_of_projective Module.Projective.of_free Module.Free.finsupp Module.Free.self Module.Finite.finsupp Module.Finite.self
instFinitePresentationForall 📖	mathematical	—	Module.FinitePresentation Ring.toSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Pi.Function.module Semiring.toModule	—	Module.finitePresentation_of_projective Module.Projective.of_free Module.Free.function Module.Free.self Module.Finite.pi Module.Finite.self
instFinitePresentationLocalizationLocalizedModule 📖	mathematical	—	Module.FinitePresentation Localization CommRing.toCommMonoid LocalizedModule CommRing.toCommSemiring AddCommGroup.toAddCommMonoid OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModule	—	FinitePresentation.of_isBaseChange IsScalarTower.left IsScalarTower.right OreLocalization.instIsScalarTower_1 isLocalizedModule_iff_isBaseChange Localization.isLocalization localizedModuleIsLocalizedModule
instFinitePresentationTensorProduct 📖	mathematical	—	Module.FinitePresentation TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid Algebra.toModule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass	—	Algebra.to_smulCommClass Module.Finite.exists_fin' instFiniteOfFinitePresentation Module.finitePresentation_of_projective Module.Projective.tensorProduct IsScalarTower.right Module.Projective.of_free Module.Free.self Module.Free.function Finite.of_fintype Module.Finite.base_change Module.Finite.pi Module.Finite.self Module.finitePresentation_of_surjective LinearMap.lTensor_surjective lTensor_exact LinearMap.exact_subtype_ker_map RingHomSurjective.ids LinearMap.exact_iff Module.Finite.of_fg Module.FinitePresentation.fg_ker Submodule.fg_range
instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation 📖	mathematical	—	IsLocalizedModule CommRing.toCommSemiring LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm LocalizedModule OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OreLocalization.instModule LinearMap.addCommMonoid LinearMap.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 LocalizedModule.map	—	Module.FinitePresentation.isLocalizedModule_mapExtendScalars localizedModuleIsLocalizedModule Localization.isLocalization

---

← Back to Index