RingHomProperties

📁 Source: Mathlib/RingTheory/RingHomProperties.lean

Statistics

Metric	Count
Definitions CodescendsAlong, IsStableUnderBaseChange, RespectsIso, StableUnderComposition, toMorphismProperty	5
Theorems algebraMap_tensorProduct, and, includeRight, mk, and, mk, pushout_inl, and, arrow_mk_iso_iff, cancel_left_isIso, cancel_right_isIso, isLocalization_away_iff, and, respectsIso, isStableUnderCobaseChange_toMorphismProperty_iff, toMorphismProperty_respectsIso_iff	16
Total	21

RingHom

Definitions

Name	Category	Theorems
CodescendsAlong 📖	MathDef	7 math math: CodescendsAlong.mk, FiniteType.codescendsAlong_faithfullyFlat, FaithfullyFlat.codescendsAlong_surjective, FinitePresentation.codescendsAlong_faithfullyFlat, Finite.codescendsAlong_faithfullyFlat, FaithfullyFlat.codescendsAlong_bijective, FaithfullyFlat.codescendsAlong_injective
IsStableUnderBaseChange 📖	MathDef	19 math math: isStableUnderCobaseChange_toMorphismProperty_iff, IsStandardOpenImmersion.isStableUnderBaseChange, FormallyUnramified.isStableUnderBaseChange, Flat.isStableUnderBaseChange, FormallySmooth.isStableUnderBaseChange, IsStableUnderBaseChange.mk, FaithfullyFlat.isStableUnderBaseChange, Bijective.isStableUnderBaseChange, isIntegral_isStableUnderBaseChange, EssFiniteType.isStableUnderBaseChange, finiteType_isStableUnderBaseChange, Etale.isStableUnderBaseChange, Smooth.isStableUnderBaseChange, finite_isStableUnderBaseChange, isStandardSmooth_isStableUnderBaseChange, isStandardSmoothOfRelativeDimension_isStableUnderBaseChange, finitePresentation_isStableUnderBaseChange, surjective_isStableUnderBaseChange, QuasiFinite.isStableUnderBaseChange
RespectsIso 📖	MathDef	22 math math: Bijective.respectsIso, StableUnderComposition.respectsIso, LocalizationAwayPreserves.respectsIso, finitePresentation_respectsIso, isIntegral_respectsIso, IsStandardOpenImmersion.respectsIso, QuasiFinite.respectsIso, isStandardSmooth_respectsIso, Flat.respectsIso, finite_respectsIso, FormallyUnramified.respectsIso, finiteType_respectsIso, injective_respectsIso, EssFiniteType.respectsIso, FaithfullyFlat.respectsIso, toMorphismProperty_respectsIso_iff, Etale.respectsIso, isStandardSmoothOfRelativeDimension_respectsIso, surjective_respectsIso, StableUnderCompositionWithLocalizationAway.respectsIso, FormallySmooth.respectsIso, PropertyIsLocal.respectsIso
StableUnderComposition 📖	MathDef	17 math math: Smooth.stableUnderComposition, IsStandardOpenImmersion.stableUnderComposition, finitePresentation_stableUnderComposition, Etale.stableUnderComposition, FaithfullyFlat.stableUnderComposition, QuasiFinite.stableUnderComposition, FormallyUnramified.stableUnderComposition, isStandardSmooth_stableUnderComposition, finiteType_stableUnderComposition, FormallySmooth.stableUnderComposition, finite_stableUnderComposition, injective_stableUnderComposition, surjective_stableUnderComposition, Flat.stableUnderComposition, Bijective.stableUnderComposition, EssFiniteType.stableUnderComposition, isIntegral_stableUnderComposition
toMorphismProperty 📖	CompOp	2 math math: isStableUnderCobaseChange_toMorphismProperty_iff, toMorphismProperty_respectsIso_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStableUnderCobaseChange_toMorphismProperty_iff 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange CommRingCat CommRingCat.instCategory toMorphismProperty IsStableUnderBaseChange	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.of_isPushout CategoryTheory.IsPushout.flip CommRingCat.isPushout_iff_isPushout IsScalarTower.of_algebraMap_eq' IsScalarTower.of_algebraMap_eq CategoryTheory.CommSq.w CategoryTheory.IsPushout.toCommSq Algebra.IsPushout.symm
toMorphismProperty_respectsIso_iff 📖	mathematical	—	RespectsIso CategoryTheory.MorphismProperty.RespectsIso CommRingCat CommRingCat.instCategory toMorphismProperty	—	CategoryTheory.MorphismProperty.RespectsIso.postcomp CategoryTheory.Iso.isIso_hom CategoryTheory.MorphismProperty.RespectsIso.precomp

RingHom.CodescendsAlong

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_tensorProduct 📖	—	RingHom.CodescendsAlong algebraMap CommRing.toCommSemiring CommSemiring.toSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Algebra.TensorProduct.instCommRing Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	—	Algebra.to_smulCommClass Algebra.TensorProduct.right_isScalarTower TensorProduct.isScalarTower_left IsScalarTower.right TensorProduct.isPushout'
and 📖	—	RingHom.CodescendsAlong	—	—	—
includeRight 📖	—	RingHom.CodescendsAlong algebraMap CommRing.toCommSemiring CommSemiring.toSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instCommRing AlgHom.toRingHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra Algebra.TensorProduct.includeRight	—	—	Algebra.to_smulCommClass TensorProduct.isScalarTower_left IsScalarTower.right Algebra.TensorProduct.right_isScalarTower TensorProduct.isPushout
mk 📖	mathematical	RingHom.RespectsIso algebraMap CommRing.toCommSemiring CommSemiring.toSemiring	RingHom.CodescendsAlong	—	Algebra.to_smulCommClass Algebra.IsPushout.symm AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass RingHom.ext AlgEquiv.commutes

RingHom.IsStableUnderBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and 📖	—	RingHom.IsStableUnderBaseChange	—	—	—
mk 📖	mathematical	RingHom.RespectsIso TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing algebraMap Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	RingHom.IsStableUnderBaseChange	—	Algebra.to_smulCommClass RingHomInvPair.ids Algebra.IsPushout.out Algebra.IsPushout.symm LinearMap.IsScalarTower.compatibleSMul TensorProduct.isScalarTower_left IsScalarTower.right TensorProduct.ext' Algebra.smul_def map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass LinearEquiv.left_inv LinearEquiv.right_inv AddHom.map_add' RingHom.ext map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one
pushout_inl 📖	mathematical	RingHom.IsStableUnderBaseChange RingHom.RespectsIso CommRingCat.carrier CommRingCat.commRing CommRingCat.Hom.hom	CategoryTheory.Limits.pushout CommRingCat CommRingCat.instCategory CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span CategoryTheory.Limits.pushout.inl	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv CommRingCat.hom_comp RingHom.RespectsIso.cancel_right_isIso CategoryTheory.Iso.isIso_inv Algebra.to_smulCommClass Algebra.TensorProduct.right_isScalarTower TensorProduct.isScalarTower_left IsScalarTower.right TensorProduct.isPushout'

RingHom.RespectsIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and 📖	—	RingHom.RespectsIso	—	—	—
arrow_mk_iso_iff 📖	mathematical	RingHom.RespectsIso	CommRingCat.carrier CommRingCat.commRing CommRingCat.Hom.hom	—	RingHom.toMorphismProperty_respectsIso_iff CategoryTheory.MorphismProperty.arrow_mk_iso_iff
cancel_left_isIso 📖	mathematical	RingHom.RespectsIso	CommRingCat.carrier CommRingCat.commRing RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.Hom.hom	—	CategoryTheory.IsIso.inv_hom_id_assoc
cancel_right_isIso 📖	mathematical	RingHom.RespectsIso	CommRingCat.carrier CommRingCat.commRing RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.Hom.hom	—	CategoryTheory.Category.assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id
isLocalization_away_iff 📖	mathematical	RingHom.RespectsIso	Localization.Away CommSemiring.toCommMonoid CommRing.toCommSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm Localization.awayMap IsLocalization.Away.map	—	Localization.isLocalization cancel_left_isIso CategoryTheory.Iso.isIso_hom cancel_right_isIso RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_pow IsLocalization.ringHom_ext RingHom.ext IsLocalization.map_eq RingHomCompTriple.comp_apply RingHomCompTriple.right_ids

RingHom.StableUnderComposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and 📖	—	RingHom.StableUnderComposition	—	—	—
respectsIso 📖	mathematical	RingHom.StableUnderComposition RingEquiv.toRingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	RingHom.RespectsIso	—	—

---

← Back to Index