Projective

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

Statistics

Metric	Count
Definitions Projective	1
Theorems surjective_linearMapComp_left, exists_rightInverse_of_surjective, iff_split, iff_split', iff_split_of_projective, of_basis, of_equiv, of_free, of_lifting_property, of_lifting_property', of_lifting_property'', of_ringEquiv, of_split, out, tensorProduct, instProjectiveDFinsupp, instProjectiveProd, projective_def, projective_def', projective_lifting_property	20
Total	21

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
surjective_linearMapComp_left 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	LinearMap.comp RingHomCompTriple.ids	—	LinearMap.surjective_comp_left_of_exists_rightInverse RingHomCompTriple.ids RingHomInvPair.ids LinearMap.exists_rightInverse_of_surjective LinearMap.range_eq_top_of_surjective RingHomSurjective.ids

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_rightInverse_of_surjective 📖	mathematical	range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Top.top Submodule Submodule.instTop	comp RingHomCompTriple.ids id	—	RingHomSurjective.ids Module.projective_lifting_property range_eq_top

Module

Definitions

Name	Category	Theorems
Projective 📖	CompData	33 math math: projective_of_isLocalizedModule, Projective.of_lifting_property', Algebra.FormallySmooth.projective_kaehlerDifferential, basicOpen_subset_freeLocus_iff, projective_of_isSemisimpleRing, Algebra.FormallySmooth.iff_subsingleton_and_projective, IsProjective.iff_projective, IsAzumaya.toProjective, freeLocus_eq_univ_iff, Algebra.FormallyUnramified.projective_of_restrictScalars, Submodule.projective_units, Submodule.projective_of_isUnit, projective_of_semisimple_ring, Projective.of_basis, Invertible.instProjective, Projective.of_equiv, Projective.of_free, Projective.iff_split_of_projective, Projective.of_lifting_property, projective_def', dual_projective, Projective.of_lifting_property'', ModuleCat.projective_of_module_projective, Projective.tensorProduct, Algebra.formallySmooth_iff, projective_def, Projective.of_split, Grassmannian.projective_quotient, instProjectiveProd, Projective.iff_split, Flat.projective_of_finitePresentation, Projective.iff_split', Projective.of_ringEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instProjectiveDFinsupp 📖	mathematical	Projective	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module	—	Projective.of_lifting_property'' RingHomCompTriple.ids DFunLike.congr_fun DFinsupp.lhom_ext' LinearMap.ext DFinsupp.ext DFinsupp.coprodMap_apply_single projective_lifting_property
instProjectiveProd 📖	mathematical	—	Projective Prod.instAddCommMonoid Prod.instModule	—	Projective.of_lifting_property'' RingHomCompTriple.ids projective_lifting_property LinearMap.comp_coprod LinearMap.coprod_inl_inr
projective_def 📖	mathematical	—	Projective Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap RingHom.id Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Finsupp.linearCombination	—	Projective.out
projective_def' 📖	mathematical	—	Projective LinearMap.comp Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule RingHom.id RingHomCompTriple.ids Finsupp.linearCombination LinearMap.id	—	RingHomCompTriple.ids
projective_lifting_property 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	LinearMap.comp RingHomCompTriple.ids	—	RingHomCompTriple.ids Projective.out LinearMap.ext map_finsuppSum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass Function.surjInv_eq

Module.Projective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_split 📖	mathematical	—	Module.Projective LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.id	—	iff_split' UnivLE.small univLE_of_max UnivLE.self
iff_split' 📖	mathematical	—	Module.Projective LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.id	—	RingHomInvPair.ids RingHomCompTriple.ids Module.Free.of_basis LinearMap.ext LinearEquiv.apply_symm_apply of_split of_free
iff_split_of_projective 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	Module.Projective LinearMap.comp RingHomCompTriple.ids LinearMap.id	—	RingHomCompTriple.ids Module.projective_lifting_property of_split
of_basis 📖	mathematical	—	Module.Projective	—	RingHomInvPair.ids AddMonoid.nat_smulCommClass' Module.Basis.constr_apply Finsupp.smul_single' mul_one map_finsuppSum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.linearCombination_single Module.Basis.linearCombination_repr
of_equiv 📖	mathematical	—	Module.Projective	—	RingHomInvPair.ids of_split RingHomCompTriple.ids LinearEquiv.symm_trans_self
of_free 📖	mathematical	—	Module.Projective	—	of_basis
of_lifting_property 📖	mathematical	LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	Module.Projective	—	RingHomCompTriple.ids of_lifting_property'' RingHomInvPair.ids LinearEquiv.surjective
of_lifting_property' 📖	mathematical	LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	Module.Projective	—	RingHomCompTriple.ids of_lifting_property'' RingHomInvPair.ids LinearEquiv.surjective
of_lifting_property'' 📖	mathematical	LinearMap.comp Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule RingHom.id RingHomCompTriple.ids LinearMap.id	Module.Projective	—	RingHomCompTriple.ids Module.projective_def' Finsupp.linearCombination_surjective
of_ringEquiv 📖	mathematical	—	Module.Projective	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHomInvPair.of_ringEquiv RingEquiv.map_zero Finsupp.ext Finsupp.mapRange.congr_simp map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearMap.semilinearMapClass AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass LinearEquiv.map_smulₛₗ map_smul SemilinearMapClass.toMulActionSemiHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingEquivClass.toNonUnitalRingHomClass RingEquiv.apply_symm_apply Finsupp.sum_mapRange_index zero_smul Finsupp.sum_equivMapDomain map_finsuppSum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearEquiv.apply_symm_apply
of_split 📖	mathematical	LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.id	Module.Projective	—	RingHomCompTriple.ids Module.projective_lifting_property Finsupp.linearCombination_single one_smul LinearMap.comp_apply LinearMap.id_apply
out 📖	mathematical	—	Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap RingHom.id Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Finsupp.linearCombination	—	—
tensorProduct 📖	mathematical	—	Module.Projective TensorProduct TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass	—	IsScalarTower.to_smulCommClass of_split Finsupp.smulCommClass Algebra.to_smulCommClass of_free Module.Free.tensor Finsupp.isScalarTower IsScalarTower.right Module.Free.finsupp Module.Free.self TensorProduct.AlgebraTensorModule.curry_injective TensorProduct.isScalarTower_left RingHomCompTriple.ids LinearMap.ext Finsupp.lhom_ext' LinearMap.ext_ring

---

← Back to Index