Unramified

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

Statistics

Metric	Count
Definitions Unramified	1
Theorems of_comp, comp, holdsForLocalization, holdsForLocalizationAway, isStableUnderBaseChange, ofLocalizationPrime, ofLocalizationSpanTarget, of_comp, of_surjective, propertyIsLocal, respectsIso, stableUnderComposition, formallyUnramified_algebraMap	13
Total	14

Algebra

Definitions

Name	Category	Theorems
Unramified 📖	CompData	5 math math: exists_unramified_of_isUnramifiedAt, Unramified.of_equiv, Unramified.baseChange, Unramified.comp, Unramified.of_isLocalization_Away

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
formallyUnramified_algebraMap 📖	mathematical	—	FormallyUnramified algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Algebra.FormallyUnramified	—	FormallyUnramified.eq_1 toAlgebra_algebraMap

RingHom.FormallyEtale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_comp 📖	mathematical	—	RingHom.FormallyEtale	—	IsScalarTower.of_algebraMap_eq' Algebra.FormallyEtale.of_restrictScalars

RingHom.FormallyUnramified

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	RingHom.FormallyUnramified RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	IsScalarTower.of_algebraMap_eq' Algebra.FormallyUnramified.comp
holdsForLocalization 📖	mathematical	—	RingHom.HoldsForLocalization RingHom.FormallyUnramified	—	RingHom.formallyUnramified_algebraMap Algebra.FormallyUnramified.of_isLocalization
holdsForLocalizationAway 📖	mathematical	—	RingHom.HoldsForLocalizationAway RingHom.FormallyUnramified	—	RingHom.HoldsForLocalization.holdsForLocalizationAway holdsForLocalization
isStableUnderBaseChange 📖	mathematical	—	RingHom.IsStableUnderBaseChange RingHom.FormallyUnramified	—	respectsIso Algebra.to_smulCommClass RingHom.formallyUnramified_algebraMap Algebra.FormallyUnramified.base_change
ofLocalizationPrime 📖	mathematical	—	RingHom.OfLocalizationPrime RingHom.FormallyUnramified	—	eq_1 Algebra.unramifiedLocus_eq_univ_iff Set.eq_univ_iff_forall RingHom.instRingHomClass Ideal.IsPrime.comap PrimeSpectrum.isPrime IsScalarTower.right IsScalarTower.of_algebraMap_eq Localization.localRingHom_to_map Algebra.FormallyUnramified.comp Algebra.FormallyUnramified.instLocalization Algebra.FormallyUnramified.inst
ofLocalizationSpanTarget 📖	mathematical	—	RingHom.OfLocalizationSpanTarget RingHom.FormallyUnramified	—	eq_1 Algebra.unramifiedLocus_eq_univ_iff Set.eq_univ_iff_forall isOpen_iUnion TopologicalSpace.Opens.is_open' Set.iUnion_congr_Prop PrimeSpectrum.basicOpen_eq_zeroLocus_compl Eq.ge PrimeSpectrum.iSup_basicOpen_eq_top_iff' TopologicalSpace.Opens.mem_top Algebra.basicOpen_subset_unramifiedLocus_iff RingHom.algebraMap_toAlgebra IsScalarTower.algebraMap_eq OreLocalization.instIsScalarTower IsScalarTower.right RingHom.formallyUnramified_algebraMap
of_comp 📖	mathematical	—	RingHom.FormallyUnramified	—	IsScalarTower.of_algebraMap_eq' Algebra.FormallyUnramified.of_restrictScalars
of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	RingHom.FormallyUnramified	—	Algebra.FormallyUnramified.of_surjective Algebra.FormallyUnramified.inst
propertyIsLocal 📖	mathematical	—	RingHom.PropertyIsLocal RingHom.FormallyUnramified	—	RingHom.LocalizationPreserves.away RingHom.IsStableUnderBaseChange.localizationPreserves isStableUnderBaseChange ofLocalizationSpanTarget RingHom.OfLocalizationSpanTarget.ofLocalizationSpan RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway stableUnderComposition holdsForLocalizationAway
respectsIso 📖	mathematical	—	RingHom.RespectsIso RingHom.FormallyUnramified	—	RingHom.StableUnderComposition.respectsIso stableUnderComposition of_surjective RingEquiv.surjective
stableUnderComposition 📖	mathematical	—	RingHom.StableUnderComposition RingHom.FormallyUnramified	—	comp

---

← Back to Index