Documentation Verification Report

Free

📁 Source: Mathlib/RingTheory/Extension/Cotangent/Free.lean

Statistics

Metric	Count
Definitions	0
Theorems `cotangentRestrict_bijective_of_basis_kaehlerDifferential`, `cotangentRestrict_bijective_of_isCompl`, `disjoint_ker_toKaehler_of_linearIndependent`, `isUnit_jacobian_of_cotangentRestrict_bijective`	4
Total	4

Algebra.Generators

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cotangentRestrict_bijective_of_basis_kaehlerDifferential` 📖	mathematical	`IsCompl` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instBoundedOrder` `Set.range` `DFunLike.coe` `Module.Basis` `KaehlerDifferential` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `Module.Basis.instFunLike` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `Derivation.instFunLike` `KaehlerDifferential.D` `val`	`Function.Bijective` `Algebra.Extension.Cotangent` `toExtension` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.instAddCommGroupCotangent` `Finsupp.instAddCommMonoid` `Algebra.Extension.instModuleCotangent` `Finsupp.module` `Semiring.toModule` `LinearMap.instFunLike` `cotangentRestrict`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `cotangentRestrict_bijective_of_isCompl` `Module.Basis.span_eq` `disjoint_ker_toKaehler_of_linearIndependent` `Module.Basis.linearIndependent`
`cotangentRestrict_bijective_of_isCompl` 📖	mathematical	`IsCompl` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instBoundedOrder` `Set.range` `Submodule.span` `KaehlerDifferential` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `DFunLike.coe` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `Derivation.instFunLike` `KaehlerDifferential.D` `val` `Top.top` `Submodule` `Submodule.instTop` `Disjoint` `Algebra.Extension.CotangentSpace` `toExtension` `TensorProduct.addCommMonoid` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `Algebra.Extension.instRingOfIsScalarTower` `Algebra.Extension.algebra₂` `TensorProduct.leftModule` `Semiring.toModule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.toKaehler` `Module.Basis` `Module.Basis.instFunLike` `cotangentSpaceBasis`	`Function.Bijective` `Algebra.Extension.Cotangent` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `LinearMap` `Algebra.Extension.instAddCommGroupCotangent` `Finsupp.instAddCommMonoid` `Algebra.Extension.instModuleCotangent` `Finsupp.module` `LinearMap.instFunLike` `cotangentRestrict`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `cotangentRestrict.eq_1` `Finsupp.mapDomain_injective` `Finsupp.isCompl_range_lmapDomain_span` `IsCompl.symm` `Finsupp.lcomapDomain_eq_linearProjOfIsCompl` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Algebra.Extension.exact_cotangentComplex_toKaehler` `LinearMap.linearProjOfIsCompl_comp_bijective_of_exact` `LinearEquiv.injective` `Algebra.Extension.subsingleton_h1Cotangent` `Equiv.subsingleton` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `Submodule.map_injective_of_injective` `RingHomSurjective.ids` `Submodule.map_inf` `Submodule.map_span` `Set.range_comp` `LinearMap.ker_comp` `Submodule.map_comap_eq_of_surjective` `LinearEquiv.surjective` `Module.Basis.coe_repr_symm` `Finsupp.linearCombination_single` `one_smul` `Submodule.map.congr_simp` `Submodule.map_bot` `LinearMap.comp.congr_simp` `Set.image_congr` `toKaehler_cotangentSpaceBasis`
`disjoint_ker_toKaehler_of_linearIndependent` 📖	mathematical	`LinearIndependent` `KaehlerDifferential` `DFunLike.coe` `Derivation` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `CommSemiring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `Derivation.instFunLike` `KaehlerDifferential.D` `val`	`Disjoint` `Submodule` `Algebra.Extension.CotangentSpace` `toExtension` `TensorProduct.addCommMonoid` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `Algebra.Extension.instRingOfIsScalarTower` `Algebra.Extension.algebra₂` `TensorProduct.leftModule` `Semiring.toModule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.toKaehler` `Submodule.span` `Set.range` `Module.Basis` `Module.Basis.instFunLike` `cotangentSpaceBasis`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `disjoint_iff` `Submodule.eq_bot_iff` `Finsupp.mem_span_range_iff_exists_finsupp` `SetLike.mem_coe` `linearIndependent_iff` `map_finsuppSum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `toKaehler_cotangentSpaceBasis`

Algebra.PreSubmersivePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUnit_jacobian_of_cotangentRestrict_bijective` 📖	mathematical	`DFunLike.coe` `Module.Basis` `Algebra.Extension.Cotangent` `Algebra.Generators.toExtension` `Algebra.Presentation.toGenerators` `toPresentation` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.id` `Module.Basis.instFunLike` `LinearMap` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `RingHom.id` `Semiring.toNonAssocSemiring` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Algebra.Extension.ker` `Submodule.addCommMonoid` `Submodule.module` `Algebra.Extension.algebra₂` `LinearMap.instFunLike` `Algebra.Presentation.relation` `Algebra.Presentation.relation_mem_ker` `Function.Bijective` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finsupp.instAddCommMonoid` `Finsupp.module` `Algebra.Generators.cotangentRestrict` `map`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `jacobian`	—	`Algebra.Presentation.relation_mem_ker` `RingHomInvPair.ids` `isUnit_jacobian_of_linearIndependent_of_span_eq_top` `LinearIndependent.map'` `Module.Basis.linearIndependent` `LinearMap.ker_eq_bot_of_injective` `Function.Bijective.injective` `LinearEquiv.ker` `Set.range_comp` `RingHomSurjective.invPair` `Submodule.span_image_linearEquiv` `RingHomSurjective.ids` `Submodule.map_span` `Module.Basis.span_eq` `Submodule.map_top` `LinearMap.range_eq_top_of_surjective` `Function.Bijective.surjective` `LinearEquiv.range`

---

← Back to Index