Documentation Verification Report

LocalStructure

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

Statistics

Metric	Count
Definitions `HasStandardEtaleSurjectionOn`	1
Theorems `exists_isStandardEtale`, `exists_isStandardEtale_mvPolynomial`, `exists_hasStandardEtaleSurjectionOn`, `exists_notMem_forall_ne_mem_and_adjoin_eq_top`, `exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective`, `instQuasiFiniteOfEssFiniteTypeOfFormallyUnramified`, `isStandardEtale`, `mk`, `of_dvd`	9
Total	10

Algebra.IsEtaleAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isStandardEtale` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Algebra.IsStandardEtale` `Localization.Away` `CommRing.toCommMonoid` `OreLocalization.instCommRing` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra` `Ring.toSemiring` `CommRing.toRing`	—	`Algebra.exists_etale_of_isEtaleAt` `Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn` `Algebra.FiniteType.of_finitePresentation` `Algebra.FormallyEtale.instFormallyUnramified` `Algebra.basicOpen_subset_etaleLocus_iff_etale` `HasSubset.Subset.trans` `Set.instIsTransSubset` `PrimeSpectrum.basicOpen_mul_le_left` `Ideal.IsPrime.mul_notMem` `HasStandardEtaleSurjectionOn.isStandardEtale` `HasStandardEtaleSurjectionOn.of_dvd`

Algebra.IsSmoothAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isStandardEtale_mvPolynomial` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsScalarTower` `MvPolynomial` `Localization.Away` `CommRing.toCommMonoid` `Algebra.toSMul` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `OreLocalization.instSemiring` `Ring.toSemiring` `CommRing.toRing` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instSMulOfIsScalarTower` `Monoid.toMulAction` `IsScalarTower.right` `Algebra.IsStandardEtale` `MvPolynomial.instCommRingMvPolynomial` `OreLocalization.instCommRing`	—	`IsScalarTower.right` `exists_notMem_isStandardSmooth` `RingHom.IsStandardSmooth.exists_etale_mvPolynomial` `IsScalarTower.of_algebraMap_eq'` `IsLocalization.isPrime_of_isPrime_disjoint` `Localization.isLocalization` `Ideal.disjoint_powers_iff_notMem` `Ideal.IsPrime.isRadical` `Algebra.IsEtaleAt.exists_isStandardEtale` `Algebra.Etale.finitePresentation` `RingHom.Etale.toAlgebra` `Algebra.FormallyEtale.instLocalization` `Algebra.Etale.formallyEtale` `IsLocalization.exists_mk'_eq` `Ideal.instIsTwoSided_1` `Ideal.IsPrime.mem_of_pow_mem` `IsLocalization.Away.of_associated` `IsLocalization.Away.algebraMap_pow_isUnit` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsUnit.unit.congr_simp` `mul_comm` `IsLocalization.Away.mul'` `OreLocalization.instIsScalarTower` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap_of_tower` `AlgEquiv.map_mul'` `AlgEquiv.map_add'` `Ideal.IsPrime.mul_notMem` `Algebra.IsStandardEtale.of_equiv`

Algebra.IsUnramifiedAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_hasStandardEtaleSurjectionOn` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `HasStandardEtaleSurjectionOn`	—	`Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective` `Algebra.ZariskisMainProperty.of_finiteType` `Algebra.QuasiFinite.instLocalization` `instQuasiFiniteOfEssFiniteTypeOfFormallyUnramified` `Algebra.EssFiniteType.of_finiteType` `Algebra.Unramified.formallyUnramified` `Submodule.fg_top` `Algebra.FormallyUnramified.of_equiv` `Algebra.FormallyUnramified.instLocalization` `Ideal.IsPrime.under` `Algebra.basicOpen_subset_unramifiedLocus_iff` `Localization.awayMap_bijective_of_dvd` `dvd_mul_right` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `Subalgebra.instSubsemiringClass` `HasStandardEtaleSurjectionOn.of_dvd` `Ideal.IsPrime.mul_notMem` `Algebra.instIsStandardEtaleRing` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization` `AlgEquiv.surjective` `Algebra.exists_formallyUnramified_of_isUnramifiedAt` `IsLocalization.isPrime_of_isPrime_disjoint` `Ideal.IsPrime.mem_of_pow_mem` `instFiniteTypeAway` `IsLocalization.exists_mk'_eq` `Ideal.instIsTwoSided_1` `IsLocalization.mk'_spec` `IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap_1`
`exists_notMem_forall_ne_mem_and_adjoin_eq_top` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Algebra.adjoin` `Ideal.ResidueField` `Ideal.under` `Ideal.IsPrime.under` `Semifield.toCommSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `IsLocalRing.ResidueField.instAlgebra` `Localization.AtPrime.instAlgebraOfLiesOver` `Ideal.over_under` `instIsLocalHomAtPrimeRingHomAlgebraMap` `Set` `Set.instSingletonSet` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`Ideal.IsPrime.under` `IsArtinianRing.of_finite` `Algebra.to_smulCommClass` `IsScalarTower.right` `instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Algebra.instFiniteResidueFieldOfFormallyUnramified` `Algebra.IsIntegral.isLocalHom` `IsPurelyInseparable.isIntegral` `isPurelyInseparable_self` `Module.FaithfullyFlat.faithfulSMul` `Module.FaithfullyFlat.instOfNontrivialOfFree` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `Module.Free.self` `Algebra.EssFiniteType.of_finiteType` `Algebra.FiniteType.of_finitePresentation` `Algebra.Etale.finitePresentation` `Algebra.instEtaleOfIsStandardSmoothOfRelativeDimensionOfNatNat` `Algebra.IsStandardSmoothOfRelativeDimension.id` `Algebra.FormallyUnramified.inst` `Algebra.QuasiFinite.finite_fiber` `Algebra.QuasiFinite.instOfFinite` `Ideal.over_under` `instIsLocalHomAtPrimeRingHomAlgebraMap` `Field.exists_primitive_element` `Algebra.instFiniteResidueFieldOfQuasiFiniteAt` `Algebra.QuasiFinite.instLocalization` `Algebra.instIsSeparableResidueFieldOfIsUnramifiedAt` `Module.Finite.finiteType` `NeZero.one` `Field.instIsLocalRing` `Algebra.adjoin_singleton_one` `Algebra.adjoin_singleton_zero` `IntermediateField.adjoin_eq_top_iff` `instIsAlgebraicResidueFieldOfIsIntegral` `Algebra.IsIntegral.of_finite` `IsScalarTower.to_smulCommClass` `IsLocalRing.ResidueField.instIsScalarTower` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instIsScalarTower` `Commute.all` `Ideal.Fiber.lift_residueField_surjective` `IsArtinianRing.exists_not_mem_forall_mem_of_ne` `PrimeSpectrum.isPrime` `Ideal.Fiber.exists_smul_eq_one_tmul` `IsScalarTower.algebraMap_apply` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsIdempotentElem.one_sub_mul_self` `IsIdempotentElem.map` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Algebra.smul_def` `map_mul` `AlgHom.map_algebraMap` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_one` `one_mul` `Ideal.algebraMap_residueField_eq_zero` `Ideal.over_def` `PrimeSpectrum.ext_iff` `EmbeddingLike.apply_eq_iff_eq` `EquivLike.toEmbeddingLike` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `Ideal.instIsTwoSided_1` `map_inv₀` `eq_inv_mul_iff_mul_eq₀` `top_le_iff` `Algebra.adjoin_singleton_le` `Subalgebra.smul_mem` `Algebra.self_mem_adjoin_singleton`
`exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective` 📖	mathematical	—	`Ideal.primesOver` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Polynomial.instCommSemiringAdjoinSingleton` `Ideal.under` `Algebra.ofSubsemiring` `Algebra.id` `Subalgebra.instSubsemiringClass` `Ideal` `Function.Bijective` `Ideal.ResidueField` `Polynomial.instCommRingAdjoinSingleton` `CommRing.toRing` `Ideal.IsPrime.under` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `IsLocalRing.ResidueField.instAlgebra` `Localization.AtPrime.instAlgebraOfLiesOver` `Ideal.over_under` `instIsLocalHomAtPrimeRingHomAlgebraMap`	—	`Ideal.IsPrime.under` `Ideal.over_under` `instIsLocalHomAtPrimeRingHomAlgebraMap` `Subalgebra.instSubsemiringClass` `exists_notMem_forall_ne_mem_and_adjoin_eq_top` `Set.ext` `Ideal.LiesOver.trans` `IsScalarTower.subalgebra'` `IsScalarTower.right` `Ideal.under_liesOver_of_liesOver` `SetLike.le_def` `instIsConcreteLE` `Eq.ge` `Ideal.over_def` `Algebra.self_mem_adjoin_singleton` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsLocalRing.ResidueField.instIsScalarTower_1` `Localization.AtPrime.instIsScalarTower_1` `AlgHom.range_eq_top` `top_le_iff` `Algebra.adjoin_singleton_le` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.toRingHom_eq_coe` `IsScalarTower.coe_toAlgHom` `IsScalarTower.algebraMap_apply` `IsLocalRing.ResidueField.instIsScalarTower` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left`
`instQuasiFiniteOfEssFiniteTypeOfFormallyUnramified` 📖	mathematical	—	`Algebra.QuasiFinite`	—	`Algebra.FormallyUnramified.finite_of_free` `Algebra.to_smulCommClass` `Algebra.FormallyUnramified.base_change` `Algebra.EssFiniteType.baseChange` `Module.Free.of_divisionRing`

HasStandardEtaleSurjectionOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isStandardEtale` 📖	mathematical	`HasStandardEtaleSurjectionOn`	`Algebra.IsStandardEtale` `Localization.Away` `CommRing.toCommMonoid` `OreLocalization.instCommRing` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra` `Ring.toSemiring` `CommRing.toRing` `CommRing.toCommSemiring`	—	`Algebra.IsStandardEtale.of_surjective` `Algebra.instIsStandardEtaleRing`
`mk` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`HasStandardEtaleSurjectionOn`	—	`Algebra.IsStandardEtale.nonempty_standardEtalePresentation` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization`
`of_dvd` 📖	—	`HasStandardEtaleSurjectionOn` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing`	—	—	`IsLocalization.Away.mul'` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization` `Algebra.IsStandardEtale.of_isLocalizationAway` `Algebra.instIsStandardEtaleRing` `IsLocalization.Away.mapₐ_surjective_of_surjective`

(root)

Definitions

Name	Category	Theorems
`HasStandardEtaleSurjectionOn` 📖	MathDef	2 math math: `Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn`, `HasStandardEtaleSurjectionOn.mk`

---

← Back to Index