Documentation Verification Report

Maps

📁 Source: Mathlib/RingTheory/GradedAlgebra/Homogeneous/Maps.lean

Statistics

Metric	Count
Definitions `comap`, `map`	2
Theorems `coe_comap`, `comap_comap`, `comap_id`, `comap_mono`, `gc_map_comap`, `irrelevant_le_map_comp`, `isPrime_comap`, `le_comap_of_map_le`, `map_comp`, `map_id`, `map_le_iff_le_comap`, `map_le_of_le_comap`, `map_map`, `map_mono`, `toIdeal_comap`, `toIdeal_map`	16
Total	18

HomogeneousIdeal

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	10 math math: `toIdeal_comap`, `map_le_iff_le_comap`, `comap_id`, `isPrime_comap`, `comap_mono`, `coe_comap`, `le_comap_of_map_le`, `gc_map_comap`, `AlgebraicGeometry.ProjectiveSpectrum.comapFun_asHomogeneousIdeal`, `comap_comap`
`map` 📖	CompOp	9 math math: `map_mono`, `map_le_iff_le_comap`, `map_id`, `irrelevant_le_map_comp`, `map_le_of_le_comap`, `map_comp`, `toIdeal_map`, `gc_map_comap`, `map_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_comap` 📖	mathematical	—	`SetLike.coe` `HomogeneousIdeal` `setLike` `comap` `Set.preimage` `DFunLike.coe` `GradedRingHom` `GradedRingHom.instFunLike`	—	—
`comap_comap` 📖	mathematical	—	`comap` `GradedRingHom.comp`	—	—
`comap_id` 📖	mathematical	—	`comap` `GradedRingHom.id`	—	—
`comap_mono` 📖	mathematical	—	`Monotone` `HomogeneousIdeal` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `comap`	—	`GaloisConnection.monotone_u` `gc_map_comap`
`gc_map_comap` 📖	mathematical	—	`GaloisConnection` `HomogeneousIdeal` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `map` `comap`	—	`map_le_iff_le_comap`
`irrelevant_le_map_comp` 📖	mathematical	`HomogeneousIdeal` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `irrelevant` `map`	`HomogeneousIdeal` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `irrelevant` `map` `GradedRingHom.comp`	—	`map_comp` `LE.le.trans` `map_mono`
`isPrime_comap` 📖	mathematical	—	`Ideal.IsPrime` `toIdeal` `comap`	—	—
`le_comap_of_map_le` 📖	mathematical	`HomogeneousIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `map`	`HomogeneousIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `comap`	—	`map_le_iff_le_comap`
`map_comp` 📖	mathematical	—	`map` `GradedRingHom.comp`	—	`map_map`
`map_id` 📖	mathematical	—	`map` `GradedRingHom.id`	—	`ext` `Ideal.map_id`
`map_le_iff_le_comap` 📖	mathematical	—	`HomogeneousIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `map` `comap`	—	`Ideal.map_le_iff_le_comap` `GradedRingHom.instRingHomClass`
`map_le_of_le_comap` 📖	mathematical	`HomogeneousIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `comap`	`HomogeneousIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `map`	—	`map_le_iff_le_comap`
`map_map` 📖	mathematical	—	`map` `GradedRingHom.comp`	—	`ext` `Ideal.map_map`
`map_mono` 📖	mathematical	—	`Monotone` `HomogeneousIdeal` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `map`	—	`GaloisConnection.monotone_l` `gc_map_comap`
`toIdeal_comap` 📖	mathematical	—	`toIdeal` `comap` `Ideal.comap` `GradedRingHom` `GradedRingHom.instFunLike` `GradedRingHom.instRingHomClass`	—	—
`toIdeal_map` 📖	mathematical	—	`toIdeal` `map` `Ideal.map` `GradedRingHom` `GradedRingHom.instFunLike`	—	—

---

← Back to Index