Documentation Verification Report

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_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`	21
Total	22

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`surjective_linearMapComp_left` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `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`	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `comp` `RingHomCompTriple.ids` `id`	—	`RingHomSurjective.ids` `Module.projective_lifting_property` `range_eq_top`

Module

Definitions

Name	Category	Theorems
`Projective` 📖	CompData	36 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_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''`, `projective_of_localization_maximal'`, `Projective.of_equiv'`, `ModuleCat.projective_of_module_projective`, `Projective.tensorProduct`, `Algebra.formallySmooth_iff`, `projective_def`, `projective_of_localization_maximal`, `instProjectiveDFinsupp`, `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`	`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` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `DFunLike.coe` `LinearMap.instFunLike` `Finsupp.linearCombination`	—	`Projective.out`
`projective_def'` 📖	mathematical	—	`Projective` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `LinearMap.comp` `RingHomCompTriple.ids` `Finsupp.linearCombination` `LinearMap.id`	—	`RingHomCompTriple.ids`
`projective_lifting_property` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `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` `AddCommMonoid` `Module` `Module.Free` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.comp` `RingHomCompTriple.ids` `LinearMap.id`	—	`iff_split'` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`iff_split'` 📖	mathematical	—	`Module.Projective` `AddCommMonoid` `Module` `Module.Free` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.comp` `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` `RingHom.id` `Semiring.toNonAssocSemiring` `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`	—	`RingEquiv.map_zero` `Finsupp.ext` `Finsupp.mapRange.congr_simp` `map_add` `SemilinearMapClass.toAddHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearMap.semilinearMapClass` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `LinearEquiv.map_smulₛₗ` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `RingHomCompTriple.comp_apply` `RingHomInvPair.triples₂` `Finsupp.sum_mapRange_index` `zero_smul` `Finsupp.sum_equivMapDomain` `map_finsuppSum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearEquiv.apply_symm_apply`
`of_equiv'` 📖	mathematical	—	`Module.Projective`	—	`RingHomInvPair.ids` `of_equiv`
`of_free` 📖	mathematical	—	`Module.Projective`	—	`of_basis`
`of_lifting_property` 📖	mathematical	`LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.comp` `RingHomCompTriple.ids`	`Module.Projective` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`RingHomCompTriple.ids` `of_lifting_property''` `RingHomInvPair.ids` `LinearEquiv.surjective`
`of_lifting_property'` 📖	mathematical	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.comp` `RingHomCompTriple.ids`	`Module.Projective`	—	`RingHomCompTriple.ids` `of_lifting_property''` `RingHomInvPair.ids` `LinearEquiv.surjective`
`of_lifting_property''` 📖	mathematical	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `LinearMap.comp` `RingHomCompTriple.ids` `LinearMap.id`	`Module.Projective`	—	`RingHomCompTriple.ids` `Module.projective_def'` `Finsupp.linearCombination_surjective`
`of_ringEquiv` 📖	mathematical	—	`Module.Projective`	—	`of_equiv`
`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	—	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `DFunLike.coe` `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