RingHom

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

Statistics

Metric	Count
Definitions `GradedRingHom`, `coeToRingHom`, `comp`, `copy`, `gradedAddHom`, `gradedZeroRingHom`, `id`, `instFunLike`, `instMonoid`, `instMul`, `instOne`, `ofClass`, `toRingHom`, `«term_→+*ᵍ_»`	14
Theorems `decompose_map`, `cancel_left`, `cancel_right`, `coe_comp`, `coe_copy`, `coe_id`, `coe_inj`, `coe_mk`, `coe_mul`, `coe_ofClass`, `coe_one`, `coe_pow`, `coe_ringHom_injective`, `coe_toRingHom`, `comp_apply`, `comp_assoc`, `comp_id`, `congr_arg`, `congr_fun`, `copy_eq`, `ext`, `ext_iff`, `gradedAddHom_apply_coe`, `gradedZeroRingHom_apply_coe`, `id_apply`, `id_comp`, `instGradedFunLike`, `instRingHomClass`, `map_add`, `map_directSumDecompose`, `map_mem`, `map_mul`, `map_neg`, `map_one`, `map_sub`, `map_zero`, `mk_coe`, `mul_def`, `one_def`, `toRingHom_eq_toRingHom`, `toRingHom_id`, `map_directSumDecompose`	42
Total	56

DirectSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`decompose_map` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompose` `GradedRing.toDecomposition` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `map` `GradedRingHom.gradedAddHom` `GradedRingHom.ofClass`	—	`AddSubmonoidClass.toZeroMemClass` `sum_support_decompose` `map_sum` `RingHomClass.toAddMonoidHomClass` `decompose_sum` `AddMonoidHom.instAddMonoidHomClass` `Graded.map_mem` `Subtype.prop` `decompose_of_mem` `Subtype.coe_eta` `map_of`

GradedRingHom

Definitions

Name	Category	Theorems
`coeToRingHom` 📖	CompOp	—
`comp` 📖	CompOp	18 math math: `HomogeneousLocalization.Away.map_map`, `HomogeneousIdeal.irrelevant_le_map_comp`, `AlgebraicGeometry.Proj.map_comp`, `comp_id`, `HomogeneousLocalization.Away.map_comp`, `cancel_left`, `id_comp`, `comp_assoc`, `coe_comp`, `HomogeneousIdeal.map_comp`, `HomogeneousLocalization.map_map`, `comp_apply`, `HomogeneousLocalization.map_comp`, `HomogeneousIdeal.map_map`, `GradedAlgHom.comp_toGradedRingHom`, `cancel_right`, `mul_def`, `HomogeneousIdeal.comap_comap`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`gradedAddHom` 📖	CompOp	4 math math: `HomogeneousLocalization.NumDenSameDeg.map_num`, `HomogeneousLocalization.NumDenSameDeg.map_den`, `gradedAddHom_apply_coe`, `DirectSum.decompose_map`
`gradedZeroRingHom` 📖	CompOp	1 math math: `gradedZeroRingHom_apply_coe`
`id` 📖	CompOp	11 math math: `HomogeneousIdeal.map_id`, `id_apply`, `HomogeneousIdeal.comap_id`, `HomogeneousLocalization.Away.map_id`, `comp_id`, `AlgebraicGeometry.Proj.map_id`, `id_comp`, `HomogeneousLocalization.map_id`, `toRingHom_id`, `coe_id`, `one_def`
`instFunLike` 📖	CompOp	48 math math: `HomogeneousIdeal.toIdeal_comap`, `map_neg`, `HomogeneousLocalization.map_mk`, `gradedZeroRingHom_apply_coe`, `AlgebraicGeometry.Proj.map_preimage_basicOpen`, `id_apply`, `HomogeneousLocalization.Away.map_map`, `AlgebraicGeometry.Proj.ι_comp_map`, `instGradedFunLike`, `AlgebraicGeometry.Proj.awayι_comp_map_assoc`, `congr_fun`, `HomogeneousLocalization.Away.map_comp`, `coe_one`, `AlgebraicGeometry.Proj.sheafedSpaceMap_hom_base_hom_apply_asHomogeneousIdeal_carrier`, `map_mul`, `HomogeneousLocalization.val_localRingHom`, `map_zero`, `coe_ofClass`, `coe_ringHom_injective`, `AlgebraicGeometry.Proj.awayToSection_comp_appLE`, `coe_mk`, `GradedAlgHom.coe_mk'`, `coe_comp`, `AlgebraicGeometry.Proj.germ_map_sectionInBasicOpen`, `HomogeneousLocalization.map_map`, `gradedAddHom_apply_coe`, `congr_arg`, `coe_toRingHom`, `map_sub`, `coe_id`, `map_directSumDecompose`, `HomogeneousIdeal.coe_comap`, `toRingHom_eq_toRingHom`, `comp_apply`, `HomogeneousIdeal.toIdeal_map`, `coe_mul`, `AlgebraicGeometry.Proj.mapAffineOpenCover_f`, `HomogeneousLocalization.map_comp`, `coe_copy`, `coe_pow`, `ext_iff`, `map_add`, `mk_coe`, `instRingHomClass`, `HomogeneousLocalization.Away.map_mk`, `AlgebraicGeometry.Proj.awayToSection_comp_appLE_assoc`, `AlgebraicGeometry.Proj.awayι_comp_map`, `map_one`
`instMonoid` 📖	CompOp	1 math math: `coe_pow`
`instMul` 📖	CompOp	2 math math: `coe_mul`, `mul_def`
`instOne` 📖	CompOp	2 math math: `coe_one`, `one_def`
`ofClass` 📖	CompOp	3 math math: `GradedAlgHom.toGradedRingHom_ofClass`, `coe_ofClass`, `DirectSum.decompose_map`
`toRingHom` 📖	CompOp	4 math math: `map_mem`, `toRingHom_id`, `coe_toRingHom`, `toRingHom_eq_toRingHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_left` 📖	mathematical	`DFunLike.coe` `GradedRingHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `GradedRingHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `ext_iff`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `GradedRingHom` `instFunLike`	`DFunLike.coe` `GradedRingHom` `instFunLike` `copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike` `id`	—	—
`coe_inj` 📖	—	`DFunLike.coe` `GradedRingHom` `instFunLike`	—	—	`DFunLike.coe_injective`
`coe_mk` 📖	mathematical	`SetLike.instMembership` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`DFunLike.coe` `GradedRingHom` `instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike` `instMul`	—	—
`coe_ofClass` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike` `ofClass`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike` `instOne`	—	—
`coe_pow` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike` `Monoid.toPow` `instMonoid` `Nat.iterate`	—	—
`coe_ringHom_injective` 📖	mathematical	—	`GradedRingHom` `RingHom` `Semiring.toNonAssocSemiring` `RingHomClass.toRingHom` `instFunLike` `instRingHomClass`	—	`instRingHomClass` `ext` `DFunLike.congr_fun`
`coe_toRingHom` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `toRingHom` `GradedRingHom` `instFunLike`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`congr_arg` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike`	—	`DFunLike.congr_arg`
`congr_fun` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike`	—	`DFunLike.congr_fun`
`copy_eq` 📖	mathematical	`DFunLike.coe` `GradedRingHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`ext` 📖	—	`DFunLike.coe` `GradedRingHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike`	—	`ext`
`gradedAddHom_apply_coe` 📖	mathematical	—	`SetLike.instMembership` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `gradedAddHom` `GradedRingHom` `instFunLike`	—	—
`gradedZeroRingHom_apply_coe` 📖	mathematical	—	`SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `SetLike.GradeZero.instSemiring` `RingHom.instFunLike` `gradedZeroRingHom` `GradedRingHom` `instFunLike`	—	—
`id_apply` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instGradedFunLike` 📖	mathematical	—	`GradedFunLike` `GradedRingHom` `instFunLike`	—	`map_mem`
`instRingHomClass` 📖	mathematical	—	`RingHomClass` `GradedRingHom` `Semiring.toNonAssocSemiring` `instFunLike`	—	`MonoidHom.map_mul'` `OneHom.map_one'` `RingHom.map_add'` `RingHom.map_zero'`
`map_add` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `instRingHomClass`
`map_directSumDecompose` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike` `SetLike.instMembership` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose` `GradedRing.toDecomposition`	—	`map_directSumDecompose` `instGradedFunLike` `instRingHomClass`
`map_mem` 📖	mathematical	`SetLike.instMembership`	`SetLike.instMembership` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `toRingHom`	—	—
`map_mul` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `instRingHomClass`
`map_neg` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `Ring.toSemiring` `instFunLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`map_neg` `RingHomClass.toAddMonoidHomClass` `instRingHomClass`
`map_one` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `instRingHomClass`
`map_sub` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `Ring.toSemiring` `instFunLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`map_sub` `RingHomClass.toAddMonoidHomClass` `instRingHomClass`
`map_zero` 📖	mathematical	—	`DFunLike.coe` `GradedRingHom` `instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `instRingHomClass`
`mk_coe` 📖	mathematical	`DFunLike.coe` `GradedRingHom` `instFunLike` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `OneHom.toFun` `MulOne.toMul` `MonoidHom.toOneHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddZero.toAdd` `SetLike.instMembership` `RingHom` `RingHom.instFunLike`	`Semiring.toNonAssocSemiring` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MulOne.toOne` `DFunLike.coe` `GradedRingHom` `instFunLike`	—	`ext`
`mul_def` 📖	mathematical	—	`GradedRingHom` `instMul` `comp`	—	—
`one_def` 📖	mathematical	—	`GradedRingHom` `instOne` `id`	—	—
`toRingHom_eq_toRingHom` 📖	mathematical	—	`RingHomClass.toRingHom` `GradedRingHom` `instFunLike` `Semiring.toNonAssocSemiring` `instRingHomClass` `toRingHom`	—	`instRingHomClass`
`toRingHom_id` 📖	mathematical	—	`toRingHom` `id` `RingHom.id` `Semiring.toNonAssocSemiring`	—	—

(root)

Definitions

Name	Category	Theorems
`GradedRingHom` 📖	CompData	51 math math: `HomogeneousIdeal.toIdeal_comap`, `GradedRingHom.map_neg`, `HomogeneousLocalization.map_mk`, `GradedRingHom.gradedZeroRingHom_apply_coe`, `AlgebraicGeometry.Proj.map_preimage_basicOpen`, `GradedRingHom.id_apply`, `HomogeneousLocalization.Away.map_map`, `AlgebraicGeometry.Proj.ι_comp_map`, `GradedRingHom.instGradedFunLike`, `AlgebraicGeometry.Proj.awayι_comp_map_assoc`, `GradedRingHom.congr_fun`, `HomogeneousLocalization.Away.map_comp`, `GradedRingHom.coe_one`, `AlgebraicGeometry.Proj.sheafedSpaceMap_hom_base_hom_apply_asHomogeneousIdeal_carrier`, `GradedRingHom.map_mul`, `HomogeneousLocalization.val_localRingHom`, `GradedRingHom.map_zero`, `GradedRingHom.coe_ofClass`, `GradedRingHom.coe_ringHom_injective`, `AlgebraicGeometry.Proj.awayToSection_comp_appLE`, `GradedRingHom.coe_mk`, `GradedAlgHom.coe_mk'`, `GradedRingHom.coe_comp`, `AlgebraicGeometry.Proj.germ_map_sectionInBasicOpen`, `HomogeneousLocalization.map_map`, `GradedRingHom.gradedAddHom_apply_coe`, `GradedAlgHom.toGradedRingHom_injective`, `GradedRingHom.congr_arg`, `GradedRingHom.coe_toRingHom`, `GradedRingHom.map_sub`, `GradedRingHom.coe_id`, `GradedRingHom.map_directSumDecompose`, `HomogeneousIdeal.coe_comap`, `GradedRingHom.toRingHom_eq_toRingHom`, `GradedRingHom.comp_apply`, `HomogeneousIdeal.toIdeal_map`, `GradedRingHom.coe_mul`, `AlgebraicGeometry.Proj.mapAffineOpenCover_f`, `HomogeneousLocalization.map_comp`, `GradedRingHom.coe_copy`, `GradedRingHom.coe_pow`, `GradedRingHom.ext_iff`, `GradedRingHom.map_add`, `GradedRingHom.one_def`, `GradedRingHom.mk_coe`, `GradedRingHom.instRingHomClass`, `HomogeneousLocalization.Away.map_mk`, `AlgebraicGeometry.Proj.awayToSection_comp_appLE_assoc`, `GradedRingHom.mul_def`, `AlgebraicGeometry.Proj.awayι_comp_map`, `GradedRingHom.map_one`
`«term_→+*ᵍ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_directSumDecompose` 📖	mathematical	—	`DFunLike.coe` `SetLike.instMembership` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose` `GradedRing.toDecomposition`	—	`DirectSum.decompose_map` `DirectSum.map_apply`

---

← Back to Index