Structures · Algebra
Module.Projective
An R-module is projective if it is a direct summand of a free module, or equivalently if maps from the module lift along surjections. There are several other equivalent definitions.
- Defined in
- Mathlib.Algebra.Module.Projective
- Shape
- 2 explicit arguments · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- Localization
How is a type an instance?
Loading the hierarchy index…
Assumed by68
- Module.projective_lifting_property
- Module.Projective.of_equiv
- dualTensorHomEquiv
- Module.Projective.of_split
- LinearMap.exists_rightInverse_of_surjective
- dualTensorHom_bijective
- Module.eval_apply_injective
- Module.forall_dual_apply_eq_zero_iff
- lTensorHomEquivHomLTensor
- AlgEquiv.eq_linearEquivConjAlgEquiv
- Module.Projective.exists_dual_ne_zero
- Module.Finite.exists_comp_eq_id_of_projective
- rTensorHomEquivHomRTensor
- Module.Projective.of_equiv'
- Module.finitePresentation_of_projective
- Module.subsingleton_dual_iff
- Module.projective_of_isLocalizedModule
- LinearMap.id_separatingRight
- Module.Projective.out
- homTensorHomEquiv
- Module.eval_ker
- Module.nontrivial_dual_iff
- rTensorHomEquivHomRTensor_apply
- LinearMap.eval_separatingLeft
- LinearMap.id_nondegenerate
- Module.Projective.exists_dual_eq_one
- Submodule.dualAnnihilator_eq_top_iff
- lTensorHomEquivHomLTensor_apply
- Module.Projective.iff_split_of_projective
- homTensorHomEquiv_toLinearMap
- rTensorHomEquivHomRTensor_toLinearMap
- lTensorHomEquivHomLTensor_toLinearMap
- Module.End.mulSemiringActionToAlgEquiv_conjAct_surjective
- Function.Surjective.surjective_linearMapComp_left
- Submodule.span_eq_top_of_ne_zero
- homTensorHomEquiv_apply
- Module.Projective.tensorProduct
- Module.eval_apply_eq_zero_iff
- Algebra.FormallyUnramified.projective_of_restrictScalars
- Module.map_eval_injective
- Module.instProjectiveProd
- Module.dual_projective
- Module.Flat.of_projective
- Submodule.dualAnnihilator_eq_bot_iff
- LinearMap.dualPairing_nondegenerate
- Module.finitePresentation_of_projective_of_exact
- Module.comap_eval_surjective
- LinearMap.eval_nondegenerate
- Module.Projective.of_ringEquiv
- Module.instIsReflexiveOfFiniteOfProjective
Ancestors0
No ancestors.