Documentation Verification Report

Locus

📁 Source: Mathlib/RingTheory/Unramified/Locus.lean

Statistics

Metric	Count
Definitions `IsUnramifiedAt`, `unramifiedLocus`	2
Theorems `comp`, `of_restrictScalars`, `residueField`, `basicOpen_subset_unramifiedLocus_iff`, `exists_formallyUnramified_of_isUnramifiedAt`, `exists_unramified_of_isUnramifiedAt`, `instFormallyUnramifiedAtPrimeOfIsUnramifiedAt`, `isOpen_unramifiedLocus`, `unramifiedLocus_eq_compl_support`, `unramifiedLocus_eq_univ_iff`	10
Total	12

Algebra

Definitions

Name	Category	Theorems
`IsUnramifiedAt` 📖	MathDef	9 math math: `IsUnramifiedAt.residueField`, `IsUnramifiedAt.of_liesOver_of_ne_bot`, `isUnramifiedAt_iff_map_eq`, `isUnramifiedAt_iff_of_isDedekindDomain`, `dvd_differentIdeal_iff`, `IsUnramifiedAt.of_liesOver`, `not_dvd_differentIdeal_iff`, `IsUnramifiedAt.of_restrictScalars`, `IsUnramifiedAt.comp`
`unramifiedLocus` 📖	CompOp	5 math math: `basicOpen_subset_unramifiedLocus_iff`, `unramifiedLocus_eq_compl_support`, `unramifiedLocus_eq_univ_iff`, `isOpen_unramifiedLocus`, `etaleLocus_eq_unramfiedLocus_inter_smoothLocus`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basicOpen_subset_unramifiedLocus_iff` 📖	mathematical	—	`Set` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.instHasSubset` `SetLike.coe` `TopologicalSpace.Opens` `PrimeSpectrum.zariskiTopology` `TopologicalSpace.Opens.instSetLike` `PrimeSpectrum.basicOpen` `unramifiedLocus` `FormallyUnramified` `Localization.Away` `CommRing.toCommMonoid` `OreLocalization.instCommRing` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra` `Ring.toSemiring` `CommRing.toRing`	—	`to_smulCommClass` `unramifiedLocus_eq_compl_support` `Set.subset_compl_comm` `PrimeSpectrum.basicOpen_eq_zeroLocus_compl` `compl_compl` `LocalizedModule.subsingleton_iff_support_subset` `formallyUnramified_iff` `Equiv.subsingleton_congr` `RingHomInvPair.ids` `IsScalarTower.left` `IsScalarTower.right` `OreLocalization.instSMulCommClass` `OreLocalization.instIsScalarTower` `KaehlerDifferential.isLocalizedModule_map` `Localization.isLocalization`
`exists_formallyUnramified_of_isUnramifiedAt` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `FormallyUnramified` `Localization.Away` `CommRing.toCommMonoid` `OreLocalization.instCommRing` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra` `Ring.toSemiring` `CommRing.toRing`	—	`TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `PrimeSpectrum.isBasis_basic_opens` `isOpen_unramifiedLocus` `basicOpen_subset_unramifiedLocus_iff`
`exists_unramified_of_isUnramifiedAt` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Unramified` `Localization.Away` `CommRing.toCommMonoid` `OreLocalization.instCommRing` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra` `Ring.toSemiring` `CommRing.toRing`	—	`exists_formallyUnramified_of_isUnramifiedAt` `EssFiniteType.of_finiteType` `FiniteType.trans` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `IsLocalization.finiteType_of_monoid_fg` `Localization.isLocalization` `Monoid.powers_fg`
`instFormallyUnramifiedAtPrimeOfIsUnramifiedAt` 📖	mathematical	—	`FormallyUnramified` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Localization.AtPrime.instAlgebraOfLiesOver`	—	`FormallyUnramified.of_restrictScalars` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left`
`isOpen_unramifiedLocus` 📖	mathematical	—	`IsOpen` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.zariskiTopology` `unramifiedLocus`	—	`to_smulCommClass` `unramifiedLocus_eq_compl_support` `Module.support_eq_zeroLocus` `KaehlerDifferential.finite` `IsClosed.isOpen_compl` `PrimeSpectrum.isClosed_zeroLocus`
`unramifiedLocus_eq_compl_support` 📖	mathematical	—	`unramifiedLocus` `Compl.compl` `Set` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.instCompl` `Module.support` `KaehlerDifferential` `instAddCommGroupKaehlerDifferential` `KaehlerDifferential.module'` `id` `to_smulCommClass` `CommSemiring.toSemiring`	—	`Set.ext` `to_smulCommClass` `PrimeSpectrum.isPrime` `RingHomInvPair.ids` `IsScalarTower.left` `IsScalarTower.right` `OreLocalization.instSMulCommClass` `OreLocalization.instIsScalarTower` `KaehlerDifferential.isLocalizedModule_map` `Localization.isLocalization` `formallyUnramified_iff` `Equiv.subsingleton_congr`
`unramifiedLocus_eq_univ_iff` 📖	mathematical	—	`unramifiedLocus` `Set.univ` `PrimeSpectrum` `CommRing.toCommSemiring` `FormallyUnramified`	—	`to_smulCommClass` `unramifiedLocus_eq_compl_support` `compl_eq_comm` `Set.compl_univ` `Module.support_eq_empty_iff` `formallyUnramified_iff`

Algebra.IsUnramifiedAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`Algebra.IsUnramifiedAt`	—	`Algebra.FormallyUnramified.of_restrictScalars` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `Algebra.FormallyUnramified.comp`
`of_restrictScalars` 📖	mathematical	—	`Algebra.IsUnramifiedAt`	—	`Algebra.FormallyUnramified.of_restrictScalars` `OreLocalization.instIsScalarTower` `IsScalarTower.right`
`residueField` 📖	mathematical	`Ideal.comap` `Ideal.Fiber` `RingHom` `TensorProduct` `CommRing.toCommSemiring` `Ideal.ResidueField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Algebra.toModule` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id` `Algebra.TensorProduct.instSemiring` `RingHom.instFunLike` `AlgHom.toRingHom` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight` `RingHom.instRingHomClass`	`Algebra.IsUnramifiedAt` `IsLocalRing.instCommRingResidueField` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.to_smulCommClass` `IsLocalRing.ResidueField`	—	`RingHom.instRingHomClass` `RingHom.SurjectiveOnStalks.baseChange'` `Ideal.surjectiveOnStalks_residueField` `Algebra.to_smulCommClass` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `TensorProduct.isScalarTower_left` `Commute.all` `Function.Surjective.forall` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `one_mul` `Algebra.FormallyUnramified.of_surjective` `Algebra.FormallyUnramified.base_change`

---

← Back to Index