Documentation Verification Report

QuasiFinite

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

Statistics

Metric	Count
Definitions `QuasiFinite`, `QuasiFinite`, `QuasiFiniteAt`	3
Theorems `comp`, `comp_iff`, `holdsForLocalizationAway`, `isStableUnderBaseChange`, `ofLocalizationSpanTarget`, `of_comp`, `of_finite`, `of_isIntegral_of_finiteType`, `propertyIsLocal`, `respectsIso`, `stableUnderComposition`, `toAlgebra`, `quasiFinite_algebraMap`	13
Total	16

Algebra

Definitions

Name	Category	Theorems
`QuasiFinite` 📖	CompData	21 math math: `QuasiFinite.of_surjective_algHom`, `QuasiFinite.instOfIsFractionRing`, `QuasiFinite.of_restrictScalars`, `QuasiFinite.instQuotientIdeal`, `QuasiFinite.instResidueField`, `QuasiFinite.iff_of_isArtinianRing`, `QuasiFinite.iff_of_algEquiv`, `QuasiFinite.of_isLocalization`, `QuasiFinite.iff_finite_primesOver`, `quasiFinite_iff`, `QuasiFinite.baseChange`, `QuasiFinite.iff_finite_comap_preimage_singleton`, `IsUnramifiedAt.instQuasiFiniteOfEssFiniteTypeOfFormallyUnramified`, `QuasiFinite.trans`, `RingHom.QuasiFinite.toAlgebra`, `RingHom.quasiFinite_algebraMap`, `QuasiFinite.of_forall_exists_mul_mem_range`, `weaklyQuasiFiniteAt_iff`, `QuasiFinite.instOfFinite`, `QuasiFinite.of_isIntegral_of_finiteType`, `QuasiFinite.instLocalization`

RingHom

Definitions

Name	Category	Theorems
`QuasiFinite` 📖	MathDef	15 math math: `AlgebraicGeometry.LocallyQuasiFinite.quasiFinite_appLE`, `AlgebraicGeometry.locallyQuasiFinite_iff`, `QuasiFinite.propertyIsLocal`, `QuasiFinite.holdsForLocalizationAway`, `QuasiFinite.comp_iff`, `QuasiFinite.ofLocalizationSpanTarget`, `QuasiFinite.stableUnderComposition`, `QuasiFinite.respectsIso`, `QuasiFinite.of_comp`, `quasiFinite_algebraMap`, `QuasiFinite.of_isIntegral_of_finiteType`, `AlgebraicGeometry.instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite`, `QuasiFinite.comp`, `QuasiFinite.isStableUnderBaseChange`, `QuasiFinite.of_finite`
`QuasiFiniteAt` 📖	MathDef	1 math math: `AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.quasiFiniteAt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiFinite_algebraMap` 📖	mathematical	—	`QuasiFinite` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.QuasiFinite`	—	`QuasiFinite.eq_1` `toAlgebra_algebraMap`

RingHom.QuasiFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`RingHom.QuasiFinite` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsScalarTower.of_algebraMap_eq'` `Algebra.QuasiFinite.trans` `toAlgebra`
`comp_iff` 📖	mathematical	—	`RingHom.QuasiFinite` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`of_comp` `comp`
`holdsForLocalizationAway` 📖	mathematical	—	`RingHom.HoldsForLocalizationAway` `RingHom.QuasiFinite`	—	`RingHom.quasiFinite_algebraMap` `Algebra.QuasiFinite.of_isLocalization` `IsScalarTower.left` `Algebra.QuasiFinite.instOfFinite` `Module.Finite.self`
`isStableUnderBaseChange` 📖	mathematical	—	`RingHom.IsStableUnderBaseChange` `RingHom.QuasiFinite`	—	`respectsIso` `Algebra.to_smulCommClass` `RingHom.quasiFinite_algebraMap` `Algebra.QuasiFinite.baseChange`
`ofLocalizationSpanTarget` 📖	mathematical	—	`RingHom.OfLocalizationSpanTarget` `RingHom.QuasiFinite`	—	`RingHom.ofLocalizationSpanTarget_iff_finite` `Algebra.to_smulCommClass` `RingHom.quasiFinite_algebraMap` `Algebra.QuasiFinite.finite_fiber` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `Localization.AtPrime.isLocalRing` `isNoetherian_of_isNoetherianRing_of_finite` `instIsNoetherianRingOfIsArtinianRing` `DivisionRing.instIsArtinianRing` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `injective_iff_map_eq_zero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `eq_zero_of_localization` `Ideal.IsMaximal.isPrime'` `Ideal.IsPrime.ne_top'` `Ideal.primesOver.isPrime` `top_le_iff` `Eq.trans_le` `Ideal.span_le` `Set.not_subset` `smulCommClass_self` `TensorProduct.isScalarTower_left` `Localization.isLocalization` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `AlgHomClass.toRingHomClass` `IsScalarTower.algebraMap_apply` `IsLocalization.map_eq` `AlgHom.commutes` `Commute.all` `Algebra.TensorProduct.ext` `Algebra.ext_id` `IsScalarTower.to_smulCommClass` `AlgHom.ext` `map_one` `MonoidHomClass.toOneHomClass` `one_mul` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `Module.Finite.of_injective`
`of_comp` 📖	mathematical	—	`RingHom.QuasiFinite`	—	`IsScalarTower.of_algebraMap_eq'` `Algebra.QuasiFinite.of_restrictScalars` `toAlgebra`
`of_finite` 📖	mathematical	—	`RingHom.QuasiFinite`	—	`Algebra.QuasiFinite.instOfFinite`
`of_isIntegral_of_finiteType` 📖	mathematical	`RingHom.IsIntegral` `CommRing.toRing`	`RingHom.QuasiFinite` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsScalarTower.of_algebraMap_eq'` `Algebra.IsStandardOpenImmersion.exists_away` `RingHom.IsStandardOpenImmersion.toAlgebra` `Algebra.QuasiFinite.of_isIntegral_of_finiteType`
`propertyIsLocal` 📖	mathematical	—	`RingHom.PropertyIsLocal` `RingHom.QuasiFinite`	—	`RingHom.LocalizationPreserves.away` `RingHom.IsStableUnderBaseChange.localizationPreserves` `isStableUnderBaseChange` `ofLocalizationSpanTarget` `RingHom.OfLocalizationSpanTarget.ofLocalizationSpan` `RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway` `stableUnderComposition` `holdsForLocalizationAway`
`respectsIso` 📖	mathematical	—	`RingHom.RespectsIso` `RingHom.QuasiFinite`	—	`RingHom.StableUnderComposition.respectsIso` `stableUnderComposition` `of_finite` `RingEquiv.finite`
`stableUnderComposition` 📖	mathematical	—	`RingHom.StableUnderComposition` `RingHom.QuasiFinite`	—	`comp`
`toAlgebra` 📖	mathematical	—	`Algebra.QuasiFinite` `RingHom.toAlgebra` `CommRing.toCommSemiring`	—	—

---

← Back to Index