Documentation Verification Report

FinitePresentation

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

Statistics

Metric	Count
Definitions `FinitePresentation`, `FinitePresentation`	2
Theorems `of_span_eq_top_target`, `of_span_eq_top_target_aux`, `of_span_eq_top_target_of_isLocalizationAway`, `pi`, `finitePresentation_holdsForLocalizationAway`, `finitePresentation_isLocal`, `finitePresentation_isStableUnderBaseChange`, `finitePresentation_localizationPreserves`, `finitePresentation_ofLocalizationSpanTarget`, `finitePresentation_respectsIso`, `finitePresentation_stableUnderComposition`	11
Total	13

AlgHom

Definitions

Name	Category	Theorems
`FinitePresentation` 📖	MathDef	7 math math: `MvPolynomial.finitePresentation_universalFactorizationMap`, `FinitePresentation.of_comp_finiteType`, `FinitePresentation.id`, `FinitePresentation.of_finiteType`, `FinitePresentation.of_surjective`, `FinitePresentation.comp`, `FinitePresentation.comp_surjective`

Algebra.FinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_span_eq_top_target` 📖	—	`Ideal.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Algebra.FinitePresentation` `Localization.Away` `CommRing.toCommMonoid` `OreLocalization.instSemiring` `Ring.toSemiring` `CommRing.toRing` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra`	—	—	`Ideal.span_eq_top_iff_finite` `Algebra.FiniteType.of_span_eq_top_target` `Algebra.FiniteType.of_finitePresentation` `Algebra.FiniteType.iff_quotient_mvPolynomial''` `Finsupp.mem_span_iff_linearCombination` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `map_sum` `Finset.sum_congr` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `Finsupp.linearCombination_apply_of_mem_supported` `Finset.coe_attach` `mul_comm` `sub_self` `MulZeroClass.zero_mul` `Ideal.instIsTwoSided_1` `Ideal.Quotient.lift_surjective_of_surjective` `Ideal.eq_top_iff_one` `eq_of_sub_eq_zero` `RingHom.instRingHomClass` `RingHomClass.toAddMonoidHomClass` `Ideal.Quotient.eq_zero_iff_mem` `Ideal.subset_span` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Ideal.sum_mem` `Ideal.mul_mem_right` `Finset.coe_image` `Set.image_univ` `quotient` `Finset.coe_singleton` `mvPolynomial` `self` `Finite.of_fintype` `Ideal.Quotient.liftₐ_apply` `of_span_eq_top_target_aux`
`of_span_eq_top_target_aux` 📖	—	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike` `Ideal.span` `SetLike.coe` `Finset` `Finset.instSetLike` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Algebra.FinitePresentation` `Localization.Away` `CommRing.toCommMonoid` `SetLike.instMembership` `OreLocalization.instSemiring` `Ring.toSemiring` `CommRing.toRing` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra`	—	—	`of_surjective` `RingHom.ker_fg_of_localizationSpan` `trans` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `IsLocalization.Away.finitePresentation` `Localization.isLocalization` `ker_fG_of_surjective` `IsLocalization.Away.mapₐ_surjective_of_surjective`
`of_span_eq_top_target_of_isLocalizationAway` 📖	—	`Ideal.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set.range` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsScalarTower` `Algebra.toSMul` `IsLocalization.Away` `Algebra.FinitePresentation`	—	—	`of_span_eq_top_target` `equiv` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization`
`pi` 📖	mathematical	`Algebra.FinitePresentation` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`Pi.semiring` `Pi.algebra`	—	`IsLocalization.away_of_isIdempotentElem` `Pi.single_eq_same` `mul_one` `RingHom.ker_evalRingHom` `RingHom.surjective` `instRingHomSurjectiveForallEvalRingHom` `of_span_eq_top_target_of_isLocalizationAway` `Ideal.span_single_eq_top` `IsScalarTower.of_algHom`

RingHom

Definitions

Name	Category	Theorems
`FinitePresentation` 📖	MathDef	22 math math: `finitePresentation_stableUnderComposition`, `finitePresentation_respectsIso`, `FinitePresentation.of_finiteType`, `AlgebraicGeometry.Scheme.Hom.finitePresentation_appLE`, `FinitePresentation.comp_surjective`, `finitePresentation_isLocal`, `FinitePresentation.of_comp_finiteType`, `AlgebraicGeometry.instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation`, `finitePresentation_localizationPreserves`, `AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE`, `finitePresentation_algebraMap`, `FinitePresentation.comp`, `FinitePresentation.of_bijective`, `AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_of_affine_subset`, `finitePresentation_isStableUnderBaseChange`, `AlgebraicGeometry.locallyOfFinitePresentation_iff`, `FinitePresentation.codescendsAlong_faithfullyFlat`, `FinitePresentation.of_surjective`, `FinitePresentation.id`, `finitePresentation_ofLocalizationSpanTarget`, `smooth_def`, `finitePresentation_holdsForLocalizationAway`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finitePresentation_holdsForLocalizationAway` 📖	mathematical	—	`HoldsForLocalizationAway` `FinitePresentation`	—	`finitePresentation_algebraMap` `IsLocalization.Away.finitePresentation`
`finitePresentation_isLocal` 📖	mathematical	—	`PropertyIsLocal` `FinitePresentation`	—	`LocalizationPreserves.away` `finitePresentation_localizationPreserves` `finitePresentation_ofLocalizationSpanTarget` `OfLocalizationSpanTarget.ofLocalizationSpan` `StableUnderComposition.stableUnderCompositionWithLocalizationAway` `finitePresentation_stableUnderComposition` `finitePresentation_holdsForLocalizationAway`
`finitePresentation_isStableUnderBaseChange` 📖	mathematical	—	`IsStableUnderBaseChange` `FinitePresentation`	—	`finitePresentation_respectsIso` `Algebra.to_smulCommClass` `Algebra.FinitePresentation.baseChange`
`finitePresentation_localizationPreserves` 📖	mathematical	—	`LocalizationPreserves` `FinitePresentation`	—	`IsStableUnderBaseChange.localizationPreserves` `finitePresentation_isStableUnderBaseChange`
`finitePresentation_ofLocalizationSpanTarget` 📖	mathematical	—	`OfLocalizationSpanTarget` `FinitePresentation`	—	`IsScalarTower.Algebra.ext` `Algebra.smul_def` `Algebra.FinitePresentation.of_span_eq_top_target`
`finitePresentation_respectsIso` 📖	mathematical	—	`RespectsIso` `FinitePresentation`	—	`StableUnderComposition.respectsIso` `finitePresentation_stableUnderComposition` `FinitePresentation.of_surjective` `RingEquiv.surjective` `instRingHomClass` `ker_coe_equiv` `Submodule.fg_bot`
`finitePresentation_stableUnderComposition` 📖	mathematical	—	`StableUnderComposition` `FinitePresentation`	—	`FinitePresentation.comp`

---

← Back to Index