FormallyUnramified

📁 Source: Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean

Statistics

Metric	Count
Definitions FormallyUnramified, FormallyUnramified, FormallyUnramified	3
Theorems isOpenImmersion_SpecMap_lmul, formallyUnramified_appLE, formallyUnramified_of_affine_subset, instHasRingHomPropertyFormallyUnramified, instIsMultiplicativeScheme, instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType, instIsStableUnderBaseChangeScheme, instIsStableUnderCompositionScheme, instOfIsOpenImmersionDiagonalScheme, isOpenImmersion_diagonal, of_comp, stalkMap, formallyUnramified_appLE, formallyUnramified_iff	14
Total	17

Algebra

Definitions

Name	Category	Theorems
FormallyUnramified 📖	CompData	34 math math: FormallyUnramified.inst, FormallyUnramified.localization_base, FormallyUnramified.of_isSeparable, FormallyUnramified.of_comp, basicOpen_subset_unramifiedLocus_iff, formallyUnramified_iff, FormallyUnramified.iff_map_maximalIdeal_eq, FormallyUnramified.comp, FormallyUnramified.of_surjective, FormallyUnramified.iff_isSeparable, instFormallyUnramifiedResidueField_1, RingHom.formallyUnramified_algebraMap, FormallyEtale.iff_formallyUnramified_of_field, FormallyUnramified.pi_iff, FormallyEtale.instFormallyUnramified, unramifiedLocus_eq_univ_iff, exists_formallyUnramified_of_isUnramifiedAt, FormallyUnramified.base_change, FormallyEtale.iff_formallyUnramified_and_formallySmooth, FormallyUnramified.quotient, FormallyUnramified.iff_comp_injective, instFormallyUnramifiedAtPrimeOfIsUnramifiedAt, FormallyEtale.iff_unramified_and_smooth, FormallyUnramified.localization_map, FormallyUnramified.of_restrictScalars, FormallyUnramified.of_equiv, FormallyUnramified.iff_exists_tensorProduct, FormallyUnramified.of_isLocalization, Unramified.formallyUnramified, FormallyUnramified.of_map_maximalIdeal, FormallyUnramified.iff_of_equiv, FormallyUnramified.instLocalization, FormallyUnramified.iff_comp_injective_of_small, instFormallyUnramifiedResidueField

Algebra.FormallyUnramified

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpenImmersion_SpecMap_lmul 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Spec CommRingCat.of TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Algebra.TensorProduct.instCommRing AlgebraicGeometry.Spec.map CommRingCat.ofHom AlgHom.toRingHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra Algebra.TensorProduct.lmul'	—	RingHom.instRingHomClass AlgebraicGeometry.isOpenImmersion_SpecMap_iff_of_surjective one_mul IsScalarTower.right Ideal.isIdempotentElem_iff_of_fg KaehlerDifferential.ideal_fg Ideal.cotangent_subsingleton_iff subsingleton_kaehlerDifferential

AlgebraicGeometry

Definitions

Name	Category	Theorems
FormallyUnramified 📖	CompData	9 math math: Etale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified, FormallyUnramified.of_comp, Etale.instFormallyUnramified, FormallyUnramified.instHasRingHomPropertyFormallyUnramified, FormallyUnramified.instIsMultiplicativeScheme, FormallyUnramified.instIsStableUnderBaseChangeScheme, formallyUnramified_iff, FormallyUnramified.instIsStableUnderCompositionScheme, FormallyUnramified.instOfIsOpenImmersionDiagonalScheme

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
formallyUnramified_iff 📖	mathematical	—	FormallyUnramified RingHom.FormallyUnramified CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Scheme.Opens CommRingCat.commRing CommRingCat.Hom.hom Scheme.Hom.appLE	—	—

AlgebraicGeometry.FormallyUnramified

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
formallyUnramified_appLE 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	RingHom.FormallyUnramified CommRingCat.carrier Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommRingCat.commRing CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.appLE	—	—
formallyUnramified_of_affine_subset 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	RingHom.FormallyUnramified CommRingCat.carrier Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommRingCat.commRing CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.appLE	—	AlgebraicGeometry.Scheme.Hom.formallyUnramified_appLE
instHasRingHomPropertyFormallyUnramified 📖	mathematical	—	AlgebraicGeometry.HasRingHomProperty AlgebraicGeometry.FormallyUnramified RingHom.FormallyUnramified	—	RingHom.FormallyUnramified.propertyIsLocal CategoryTheory.MorphismProperty.ext AlgebraicGeometry.formallyUnramified_iff AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen
instIsMultiplicativeScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.FormallyUnramified	—	instOfIsOpenImmersionDiagonalScheme AlgebraicGeometry.IsOpenImmersion.of_isIso AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.instIsIsoDiagonalOfMono AlgebraicGeometry.IsOpenImmersion.mono CategoryTheory.IsIso.id instIsStableUnderCompositionScheme
instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType 📖	mathematical	—	Algebra.IsSeparable CommRingCat.carrier AlgebraicGeometry.Scheme.residueField DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CommRingCat.commRing DivisionRing.toRing Field.toDivisionRing AlgebraicGeometry.Scheme.instFieldCarrierResidueField RingHom.toAlgebra Semifield.toCommSemiring Field.toSemifield CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.residueFieldMap	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Scheme.Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf RingHom.essFiniteType_algebraMap RingHom.algebraMap_toAlgebra AlgebraicGeometry.LocallyOfFiniteType.stalkMap RingHom.formallyUnramified_algebraMap stalkMap Algebra.instIsSeparableResidueFieldOfFormallyUnramified Algebra.algebra_ext IsLocalRing.residue_surjective
instIsStableUnderBaseChangeScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.FormallyUnramified	—	AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange instHasRingHomPropertyFormallyUnramified RingHom.FormallyUnramified.isStableUnderBaseChange
instIsStableUnderCompositionScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComposition AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.FormallyUnramified	—	AlgebraicGeometry.HasRingHomProperty.stableUnderComposition instHasRingHomPropertyFormallyUnramified RingHom.FormallyUnramified.stableUnderComposition
instOfIsOpenImmersionDiagonalScheme 📖	mathematical	—	AlgebraicGeometry.FormallyUnramified	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback Equiv.surjective AlgebraicGeometry.HasRingHomProperty.Spec_iff instHasRingHomPropertyFormallyUnramified TensorProduct.smulCommClass_left smulCommClass_self mul_one CategoryTheory.MorphismProperty.cancel_right_of_respectsIso AlgebraicGeometry.isOpenImmersion_respectsIso CategoryTheory.Iso.isIso_inv AlgebraicGeometry.diagonal_SpecMap RingHom.instRingHomClass AlgebraicGeometry.isOpenImmersion_SpecMap_iff_of_surjective Ideal.toCotangent_surjective Ideal.mem_span_singleton Eq.le Ideal.toCotangent_eq_zero pow_two Algebra.to_smulCommClass IsScalarTower.right mul_assoc Ideal.mul_mem_mul Eq.ge Ideal.mem_span_singleton_self AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource CategoryTheory.MorphismProperty.comp_mem AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.diagonal_isStableUnderComposition AlgebraicGeometry.isOpenImmersion_isStableUnderComposition AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Limits.pullback.instIsIsoDiagonalOfMono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.local_affine AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtTarget CategoryTheory.MorphismProperty.pullback_snd CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.IsStableUnderBaseChange.diagonal
isOpenImmersion_diagonal 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback.diagonalObj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.diagonal	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.Spec.map_surjective AlgebraicGeometry.diagonal_SpecMap CategoryTheory.MorphismProperty.cancel_right_of_respectsIso AlgebraicGeometry.isOpenImmersion_respectsIso CategoryTheory.Iso.isIso_inv Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul AlgebraicGeometry.HasRingHomProperty.Spec_iff instHasRingHomPropertyFormallyUnramified Algebra.EssFiniteType.of_finiteType AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsZariskiLocalAtTarget.of_range_subset_iSup AlgebraicGeometry.isOpenImmersion_isZariskiLocalAtTarget CategoryTheory.MorphismProperty.Respects.toRespectsRight CategoryTheory.MorphismProperty.instRespectsOfIsStableUnderComposition AlgebraicGeometry.isOpenImmersion_isStableUnderComposition AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.comp_mem instIsStableUnderCompositionScheme instOfIsOpenImmersionDiagonalScheme AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Limits.pullback.instIsIsoDiagonalOfMono AlgebraicGeometry.IsOpenImmersion.mono CategoryTheory.MorphismProperty.pullback_snd CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeScheme AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyOfFiniteType AlgebraicGeometry.locallyOfFiniteType_of_isOpenImmersion AlgebraicGeometry.locallyOfFiniteType_isStableUnderBaseChange AlgebraicGeometry.Scheme.local_affine
of_comp 📖	mathematical	—	AlgebraicGeometry.FormallyUnramified	—	AlgebraicGeometry.HasRingHomProperty.of_comp instHasRingHomPropertyFormallyUnramified IsScalarTower.of_algebraMap_eq' Algebra.FormallyUnramified.of_restrictScalars
stalkMap 📖	mathematical	—	RingHom.FormallyUnramified CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CommRingCat.commRing CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.stalkMap	—	AlgebraicGeometry.HasRingHomProperty.stalkMap instHasRingHomPropertyFormallyUnramified RingHom.HoldsForLocalization.localRingHom RingHom.FormallyUnramified.stableUnderComposition RingHom.IsStableUnderBaseChange.localizationPreserves RingHom.FormallyUnramified.isStableUnderBaseChange RingHom.FormallyUnramified.holdsForLocalization RingHom.instRingHomClass Ideal.IsPrime.comap

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
formallyUnramified_appLE 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	RingHom.FormallyUnramified CommRingCat.carrier Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommRingCat.commRing CommRingCat.Hom.hom appLE	—	AlgebraicGeometry.FormallyUnramified.formallyUnramified_appLE

RingHom

Definitions

Name	Category	Theorems
FormallyUnramified 📖	MathDef	21 math math: FormallyUnramified.of_comp, Etale.eq_formallyUnramified_and_smooth, FormallyUnramified.isStableUnderBaseChange, AlgebraicGeometry.Scheme.Hom.formallyUnramified_appLE, FormallyUnramified.comp, FormallyUnramified.stableUnderComposition, AlgebraicGeometry.FormallyUnramified.formallyUnramified_of_affine_subset, formallyUnramified_algebraMap, FormallyUnramified.ofLocalizationPrime, Etale.formallyUnramified, FormallyUnramified.respectsIso, AlgebraicGeometry.FormallyUnramified.instHasRingHomPropertyFormallyUnramified, FormallyUnramified.ofLocalizationSpanTarget, FormallyUnramified.holdsForLocalization, AlgebraicGeometry.FormallyUnramified.stalkMap, AlgebraicGeometry.formallyUnramified_iff, etale_iff_formallyUnramified_and_smooth, FormallyUnramified.holdsForLocalizationAway, AlgebraicGeometry.FormallyUnramified.formallyUnramified_appLE, FormallyUnramified.propertyIsLocal, FormallyUnramified.of_surjective

---

← Back to Index