Documentation Verification Report

Locus

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

Statistics

Metric	Count
Definitions `IsEtaleAt`, `etaleLocus`	2
Theorems `comp`, `basicOpen_subset_etaleLocus_iff`, `basicOpen_subset_etaleLocus_iff_etale`, `etaleLocus_eq_compl_support`, `etaleLocus_eq_univ_iff`, `etaleLocus_eq_univ_iff_etale`, `etaleLocus_eq_unramfiedLocus_inter_smoothLocus`, `exists_etale_of_isEtaleAt`, `isOpen_etaleLocus`, `mem_etaleLocus_iff`	10
Total	12

Algebra

Definitions

Name	Category	Theorems
`IsEtaleAt` 📖	MathDef	3 math math: `IsEtaleAt.of_isUnramifiedAt_of_flat`, `mem_etaleLocus_iff`, `IsEtaleAt.comp`
`etaleLocus` 📖	CompOp	8 math math: `basicOpen_subset_etaleLocus_iff_etale`, `etaleLocus_eq_univ_iff_etale`, `etaleLocus_eq_univ_iff`, `isOpen_etaleLocus`, `basicOpen_subset_etaleLocus_iff`, `mem_etaleLocus_iff`, `etaleLocus_eq_unramfiedLocus_inter_smoothLocus`, `etaleLocus_eq_compl_support`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basicOpen_subset_etaleLocus_iff` 📖	mathematical	—	`Set` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.instHasSubset` `SetLike.coe` `TopologicalSpace.Opens` `PrimeSpectrum.zariskiTopology` `TopologicalSpace.Opens.instSetLike` `PrimeSpectrum.basicOpen` `etaleLocus` `FormallyEtale` `Localization.Away` `CommRing.toCommMonoid` `OreLocalization.instCommRing` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra` `Ring.toSemiring` `CommRing.toRing`	—	`to_smulCommClass` `Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `etaleLocus_eq_compl_support` `Set.subset_inter_iff` `Set.subset_compl_comm` `PrimeSpectrum.basicOpen_eq_zeroLocus_compl` `compl_compl` `LocalizedModule.subsingleton_iff_support_subset` `formallyEtale_iff` `Equiv.subsingleton_congr` `RingHomInvPair.ids` `IsScalarTower.left` `OreLocalization.instSMulCommClass` `OreLocalization.instIsScalarTower` `KaehlerDifferential.isLocalizedModule_map` `Localization.isLocalization` `H1Cotangent.isLocalizedModule`
`basicOpen_subset_etaleLocus_iff_etale` 📖	mathematical	—	`Set` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.instHasSubset` `SetLike.coe` `TopologicalSpace.Opens` `PrimeSpectrum.zariskiTopology` `TopologicalSpace.Opens.instSetLike` `PrimeSpectrum.basicOpen` `etaleLocus` `Etale` `Localization.Away` `CommRing.toCommMonoid` `OreLocalization.instCommRing` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra` `Ring.toSemiring` `CommRing.toRing`	—	`basicOpen_subset_etaleLocus_iff` `instFinitePresentationAway` `Etale.formallyEtale`
`etaleLocus_eq_compl_support` 📖	mathematical	—	`etaleLocus` `Set` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.instInter` `Compl.compl` `Set.instCompl` `Module.support` `KaehlerDifferential` `instAddCommGroupKaehlerDifferential` `KaehlerDifferential.module'` `id` `to_smulCommClass` `CommSemiring.toSemiring` `H1Cotangent` `Extension.instAddCommGroupH1Cotangent` `Generators.toExtension` `Generators.self` `Extension.instModuleH1CotangentOfIsScalarTowerCotangent` `Extension.instModuleCotangent` `Extension.instIsScalarTowerCotangent` `IsScalarTower.right`	—	`Set.ext` `to_smulCommClass` `Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `PrimeSpectrum.isPrime` `RingHomInvPair.ids` `IsScalarTower.left` `OreLocalization.instSMulCommClass` `OreLocalization.instIsScalarTower` `KaehlerDifferential.isLocalizedModule_map` `Localization.isLocalization` `H1Cotangent.isLocalizedModule` `formallyEtale_iff` `Equiv.subsingleton_congr`
`etaleLocus_eq_univ_iff` 📖	mathematical	—	`etaleLocus` `Set.univ` `PrimeSpectrum` `CommRing.toCommSemiring` `FormallyEtale`	—	`to_smulCommClass` `Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `etaleLocus_eq_compl_support` `Set.compl_union` `compl_eq_comm` `Set.compl_univ` `Set.subset_empty_iff` `Set.union_subset_iff` `Module.support_eq_empty_iff` `formallyEtale_iff`
`etaleLocus_eq_univ_iff_etale` 📖	mathematical	—	`etaleLocus` `Set.univ` `PrimeSpectrum` `CommRing.toCommSemiring` `Etale`	—	`etaleLocus_eq_univ_iff` `Etale.formallyEtale`
`etaleLocus_eq_unramfiedLocus_inter_smoothLocus` 📖	mathematical	—	`etaleLocus` `Set` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.instInter` `unramifiedLocus` `smoothLocus`	—	`Set.ext` `FormallyEtale.iff_formallyUnramified_and_formallySmooth`
`exists_etale_of_isEtaleAt` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Etale` `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_etaleLocus` `basicOpen_subset_etaleLocus_iff` `FinitePresentation.of_isLocalizationAway` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization`
`isOpen_etaleLocus` 📖	mathematical	—	`IsOpen` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.zariskiTopology` `etaleLocus`	—	`etaleLocus_eq_unramfiedLocus_inter_smoothLocus` `IsOpen.inter` `isOpen_unramifiedLocus` `EssFiniteType.of_finiteType` `FiniteType.of_finitePresentation` `isOpen_smoothLocus`
`mem_etaleLocus_iff` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `etaleLocus` `IsEtaleAt` `PrimeSpectrum.asIdeal` `PrimeSpectrum.isPrime`	—	—

Algebra.IsEtaleAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`Algebra.IsEtaleAt`	—	`Algebra.FormallyEtale.localization_base` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `Localization.isLocalization` `Algebra.FormallyEtale.comp`

---

← Back to Index