Basic

📁 Source: Mathlib/RingTheory/LocalRing/RingHom/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems isLocalHom, of_surjective, instIsLocalHomRingHomOfNontrivial, local_hom_TFAE, map_maximalIdeal_le, map_maximalIdeal_lt_top, map_maximalIdeal_of_surjective, map_ringEquiv_maximalIdeal, maximalIdeal_comap, of_surjective, surjective_units_map_of_local_ringHom, isLocalRing, domain_isLocalRing, isLocalHom_comp, instIsLocalHomZModRingHomOfIsLocalRingOfNontrivial, isLocalHom_id, isLocalHom_of_comp, isLocalHom_toRingHom, map_nonunit	19
Total	19

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalHom 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	IsLocalHom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike	—	IsLocalHom.of_surjective

IsLocalHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	IsLocalHom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike	—	IsLocalRing.of_surjective' RingHom.instRingHomClass List.TFAE.out IsLocalRing.local_hom_TFAE Ideal.comap_isMaximal_of_surjective IsLocalRing.maximalIdeal.isMaximal Eq.le ExistsUnique.unique IsLocalRing.maximal_ideal_unique

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLocalHomRingHomOfNontrivial 📖	mathematical	—	IsLocalHom RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike	—	RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsUnit.ne_zero
local_hom_TFAE 📖	mathematical	—	List.TFAE IsLocalHom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike Set Set.instHasSubset Set.image DFunLike.coe SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule maximalIdeal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Ideal.map Ideal.comap RingHom.instRingHomClass	—	map_nonunit RingHom.instRingHomClass Set.image_subset_iff Ideal.map_le_iff_le_comap not_imp_not Ideal.ext not_iff_not isUnit_map_iff MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass le_of_eq List.tfae_of_cycle
map_maximalIdeal_le 📖	mathematical	—	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.map RingHom RingHom.instFunLike maximalIdeal	—	RingHom.instRingHomClass Ideal.map_le_iff_le_comap maximalIdeal_comap le_refl
map_maximalIdeal_lt_top 📖	mathematical	—	Ideal CommSemiring.toSemiring Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.map RingHom RingHom.instFunLike maximalIdeal Top.top Submodule.instTop	—	LE.le.trans_lt map_maximalIdeal_le Ideal.IsMaximal.lt_top maximalIdeal.isMaximal
map_maximalIdeal_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	Ideal.map RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike maximalIdeal	—	IsLocalHom.of_surjective toNontrivial RingHom.instRingHomClass maximalIdeal_comap Ideal.map_comap_of_surjective
map_ringEquiv_maximalIdeal 📖	mathematical	—	Ideal.map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd CommSemiring.toSemiring CommRing.toCommSemiring EquivLike.toFunLike RingEquiv.instEquivLike maximalIdeal	—	map_maximalIdeal_of_surjective RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.surjective
maximalIdeal_comap 📖	mathematical	—	Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike RingHom.instRingHomClass maximalIdeal	—	RingHom.instRingHomClass List.TFAE.out local_hom_TFAE
of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	IsLocalRing	—	of_isUnit_or_isUnit_of_isUnit_add RingHom.isUnit_map isUnit_or_isUnit_of_isUnit_add IsLocalHom.map_nonunit map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
surjective_units_map_of_local_ringHom 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Units.map RingHom.toMonoidHom Semiring.toNonAssocSemiring	—	isUnit_of_map_unit Units.isUnit Units.ext

RingEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalRing 📖	mathematical	—	IsLocalRing	—	IsLocalRing.of_surjective Equiv.nontrivial IsLocalRing.toNontrivial RingEquivClass.toRingHomClass instRingEquivClass isLocalHom_toRingHom isLocalHom_equiv RingEquivClass.toMulEquivClass surjective

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
domain_isLocalRing 📖	mathematical	—	IsLocalRing	—	IsLocalRing.of_nonunits_add domain_nontrivial IsLocalRing.toNontrivial map_mem_nonunits_iff MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass map_add IsLocalRing.nonunits_add
isLocalHom_comp 📖	mathematical	—	IsLocalHom RingHom Semiring.toNonAssocSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero instFunLike comp	—	IsLocalHom.map_nonunit

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLocalHomZModRingHomOfIsLocalRingOfNontrivial 📖	mathematical	—	IsLocalHom ZMod RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike	—	Function.Surjective.isLocalHom ZMod.ringHom_surjective
isLocalHom_id 📖	mathematical	—	IsLocalHom RingHom Semiring.toNonAssocSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike RingHom.id	—	—
isLocalHom_of_comp 📖	mathematical	—	IsLocalHom RingHom Semiring.toNonAssocSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike	—	isUnit_map_iff MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHom.isUnit_map
isLocalHom_toRingHom 📖	mathematical	—	IsLocalHom RingHom Semiring.toNonAssocSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike RingHomClass.toRingHom	—	IsLocalHom.map_nonunit
map_nonunit 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal DFunLike.coe RingHom RingHom.instFunLike	—	isUnit_of_map_unit

---

← Back to Index