Documentation Verification Report

Kaehler

📁 Source: Mathlib/RingTheory/Etale/Kaehler.lean

Statistics

Metric	Count
Definitions `tensorCotangent`, `tensorCotangentInvFun`, `tensorCotangentSpace`, `tensorH1Cotangent`, `tensorH1CotangentOfIsLocalization`, `tensorKaehlerEquivOfFormallyEtale`	6
Theorems `tensorCotangentInvFun_smul_mk`, `isLocalizedModule`, `tensorH1CotangentOfIsLocalization_toLinearMap`, `isBaseChange_of_formallyEtale`, `isLocalizedModule_map`, `span_range_map_derivation_of_isLocalization`, `tensorKaehlerEquivOfFormallyEtale_apply`, `tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap`	8
Total	14

Algebra

Definitions

Name	Category	Theorems
`tensorH1CotangentOfIsLocalization` 📖	CompOp	1 math math: `tensorH1CotangentOfIsLocalization_toLinearMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tensorH1CotangentOfIsLocalization_toLinearMap` 📖	mathematical	—	`LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `H1Cotangent` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Extension.instAddCommGroupH1Cotangent` `Generators.toExtension` `Generators.self` `toModule` `Extension.instModuleH1CotangentOfIsScalarTowerCotangent` `id` `Extension.instModuleCotangent` `Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `to_smulCommClass` `tensorH1CotangentOfIsLocalization` `LinearMap.liftBaseChange` `Extension.instIsScalarTowerH1CotangentOfCotangent` `H1Cotangent.map` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.right` `Extension.instIsScalarTowerCotangent` `Extension.instIsScalarTowerH1CotangentOfCotangent` `RingHomInvPair.ids` `to_smulCommClass` `IsScalarTower.left` `LinearMap.ext_ring` `IsScalarTower.to_smulCommClass` `LinearMap.ext` `one_smul` `Extension.H1Cotangent.equivOfFormallySmooth_symm` `LinearEquiv.symm_apply_eq` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `OreLocalization.instIsScalarTower` `Localization.isLocalization` `Extension.instIsScalarTowerRing_2` `IsLocalization.map_units` `IsLocalization.exists_mk'_eq` `Extension.algebraMap_surjective` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsLocalization.lift_mk'_spec` `AlgHom.commutes` `MvPolynomial.algHom_ext` `MvPolynomial.aeval_X` `Extension.algebraMap_σ` `Generators.algebraMap_apply` `DFunLike.congr_fun` `Extension.H1Cotangent.equivOfFormallySmooth_apply` `H1Cotangent.map.eq_1` `LinearMap.IsScalarTower.compatibleSMul` `LinearMap.coe_restrictScalars` `RingHomCompTriple.ids` `LinearMap.comp_apply` `Extension.H1Cotangent.map_comp` `Extension.H1Cotangent.map_eq`

Algebra.Extension

Definitions

Name	Category	Theorems
`tensorCotangent` 📖	CompOp	—
`tensorCotangentInvFun` 📖	CompOp	1 math math: `tensorCotangentInvFun_smul_mk`
`tensorCotangentSpace` 📖	CompOp	—
`tensorH1Cotangent` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tensorCotangentInvFun_smul_mk` 📖	mathematical	`algebraMap` `Ring` `CommRing.toCommSemiring` `commRing` `CommSemiring.toSemiring` `Hom.toRingHom` `Algebra.id` `Function.Bijective` `TensorProduct` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `ker` `Submodule.addCommMonoid` `Algebra.toModule` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `LinearMap.instFunLike` `LinearMap.liftBaseChange` `Submodule.module'` `Algebra.toSMul` `IsScalarTower.right` `Submodule.isScalarTower'` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Hom.mapKer`	`AddMonoidHom` `Cotangent` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupCotangent` `instModuleCotangent` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `TensorProduct.addZeroClass` `AddMonoidHom.instFunLike` `tensorCotangentInvFun` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `algebra₂` `RingHom` `RingHom.instFunLike` `TensorProduct.leftHasSMul` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `Submodule.isScalarTower'` `SMulCommClass.of_commMonoid` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `TensorProduct.isScalarTower_left` `IsScalarTower.of_algebraMap_eq` `Hom.algebraMap_toRingHom` `RingHomCompTriple.ids` `TensorProduct.smulCommClass_left` `smulCommClass_self` `RingHomInvPair.ids` `LinearEquiv.symm_apply_apply`

Algebra.H1Cotangent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalizedModule` 📖	mathematical	—	`IsLocalizedModule` `CommRing.toCommSemiring` `Algebra.H1Cotangent` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupH1Cotangent` `Algebra.Generators.toExtension` `Algebra.Generators.self` `Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent` `Algebra.id` `Algebra.Extension.instModuleCotangent` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `CommSemiring.toSemiring` `map` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule`	—	`Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `IsScalarTower.left` `Algebra.Extension.instIsScalarTowerH1CotangentOfCotangent` `isLocalizedModule_iff_isBaseChange` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `Algebra.tensorH1CotangentOfIsLocalization_toLinearMap` `LinearEquiv.bijective`

KaehlerDifferential

Definitions

Name	Category	Theorems
`tensorKaehlerEquivOfFormallyEtale` 📖	CompOp	2 math math: `tensorKaehlerEquivOfFormallyEtale_apply`, `tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBaseChange_of_formallyEtale` 📖	mathematical	—	`IsBaseChange` `KaehlerDifferential` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `CommRing.toCommSemiring` `module'` `Algebra.id` `Algebra.to_smulCommClass` `CommSemiring.toSemiring` `IsScalarTower.to_smulCommClass` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `isScalarTower_of_tower` `Algebra.toSMul` `IsScalarTower.right` `map` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction`	—	`Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `isScalarTower_of_tower` `IsScalarTower.right` `IsScalarTower.left` `RingHomInvPair.ids` `LinearMap.IsScalarTower.compatibleSMul` `TensorProduct.isScalarTower_left` `TensorProduct.AlgebraTensorModule.curry_injective` `LinearMap.ext` `Derivation.liftKaehlerDifferential_unique` `smulCommClass_self` `Derivation.ext` `map_D` `mapBaseChange_tmul` `LinearEquiv.bijective`
`isLocalizedModule_map` 📖	mathematical	—	`IsLocalizedModule` `CommRing.toCommSemiring` `KaehlerDifferential` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `module'` `Algebra.id` `Algebra.to_smulCommClass` `CommSemiring.toSemiring` `IsScalarTower.to_smulCommClass` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `map` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction`	—	`Algebra.FormallyEtale.of_isLocalization` `Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `isScalarTower_of_tower` `IsScalarTower.right` `isLocalizedModule_iff_isBaseChange` `isBaseChange_of_formallyEtale`
`span_range_map_derivation_of_isLocalization` 📖	mathematical	—	`Submodule.span` `KaehlerDifferential` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `module'` `Algebra.id` `Algebra.to_smulCommClass` `Set.range` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `IsScalarTower.to_smulCommClass` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `map` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `Derivation.instFunLike` `D` `Top.top` `Submodule` `Submodule.instTop`	—	`Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `smulCommClass_self` `Set.range_comp` `span_eq_top_of_isLocalizedModule` `isScalarTower_of_tower` `IsScalarTower.right` `isLocalizedModule_map` `span_range_derivation`
`tensorKaehlerEquivOfFormallyEtale_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `module'` `Algebra.id` `Algebra.to_smulCommClass` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `tensorKaehlerEquivOfFormallyEtale` `LinearMap` `LinearMap.instFunLike` `mapBaseChange`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `KaehlerDifferential` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `module'` `Algebra.id` `Algebra.to_smulCommClass` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `tensorKaehlerEquivOfFormallyEtale` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Derivation.instFunLike` `D` `RingHom` `RingHom.instFunLike` `algebraMap` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Algebra.to_smulCommClass` `RingHomInvPair.ids` `smulCommClass_self` `LinearEquiv.symm_apply_eq` `tensorKaehlerEquivOfFormallyEtale_apply` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `mapBaseChange_tmul` `one_smul` `map_D`

---

← Back to Index