Documentation Verification Report

OpenImmersion

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

Statistics

Metric	Count
Definitions `IsStandardOpenImmersion`, `IsStandardOpenImmersion`	2
Theorems `exists_away`, `trans`, `instIsStandardOpenImmersionAway`, `instIsStandardOpenImmersionTensorProduct`, `isStandardOpenImmersion_iff`, `algebraMap`, `comp`, `containsIdentities`, `holdsForLocalizationAway`, `id`, `isStableUnderBaseChange`, `of_bijective`, `respectsIso`, `stableUnderComposition`, `toAlgebra`, `isStandardOpenImmersion_algebraMap`	16
Total	18

Algebra

Definitions

Name	Category	Theorems
`IsStandardOpenImmersion` 📖	CompData	6 math math: `RingHom.IsStandardOpenImmersion.toAlgebra`, `RingHom.isStandardOpenImmersion_algebraMap`, `isStandardOpenImmersion_iff`, `instIsStandardOpenImmersionTensorProduct`, `IsStandardOpenImmersion.trans`, `instIsStandardOpenImmersionAway`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsStandardOpenImmersionAway` 📖	mathematical	—	`IsStandardOpenImmersion` `Localization.Away` `CommSemiring.toCommMonoid` `OreLocalization.instCommSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra` `CommSemiring.toSemiring` `id`	—	`Localization.isLocalization`
`instIsStandardOpenImmersionTensorProduct` 📖	mathematical	—	`IsStandardOpenImmersion` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `toModule` `TensorProduct.instCommSemiring` `TensorProduct.leftAlgebra` `id` `to_smulCommClass`	—	`to_smulCommClass` `IsStandardOpenImmersion.exists_away` `IsLocalization.Away.tensor`
`isStandardOpenImmersion_iff` 📖	mathematical	—	`IsStandardOpenImmersion` `IsLocalization.Away`	—	—

Algebra.IsStandardOpenImmersion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_away` 📖	mathematical	—	`IsLocalization.Away`	—	—
`trans` 📖	mathematical	—	`Algebra.IsStandardOpenImmersion`	—	`exists_away` `IsLocalization.Away.of_associated` `Associated.symm` `IsLocalization.Away.associated_sec_fst` `IsLocalization.Away.mul'`

RingHom

Definitions

Name	Category	Theorems
`IsStandardOpenImmersion` 📖	MathDef	10 math math: `IsStandardOpenImmersion.id`, `IsStandardOpenImmersion.isStableUnderBaseChange`, `IsStandardOpenImmersion.stableUnderComposition`, `isStandardOpenImmersion_algebraMap`, `IsStandardOpenImmersion.respectsIso`, `IsStandardOpenImmersion.comp`, `IsStandardOpenImmersion.holdsForLocalizationAway`, `IsStandardOpenImmersion.containsIdentities`, `IsStandardOpenImmersion.algebraMap`, `IsStandardOpenImmersion.of_bijective`

Theorems

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

RingHom.IsStandardOpenImmersion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap` 📖	mathematical	—	`RingHom.IsStandardOpenImmersion` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`RingHom.isStandardOpenImmersion_algebraMap`
`comp` 📖	mathematical	—	`RingHom.IsStandardOpenImmersion` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsScalarTower.of_algebraMap_eq'` `Algebra.IsStandardOpenImmersion.trans` `toAlgebra`
`containsIdentities` 📖	mathematical	—	`RingHom.ContainsIdentities` `RingHom.IsStandardOpenImmersion`	—	`id`
`holdsForLocalizationAway` 📖	mathematical	—	`RingHom.HoldsForLocalizationAway` `RingHom.IsStandardOpenImmersion`	—	`algebraMap`
`id` 📖	mathematical	—	`RingHom.IsStandardOpenImmersion` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`of_bijective` `Function.bijective_id`
`isStableUnderBaseChange` 📖	mathematical	—	`RingHom.IsStableUnderBaseChange` `RingHom.IsStandardOpenImmersion`	—	`respectsIso` `Algebra.to_smulCommClass` `RingHom.isStandardOpenImmersion_algebraMap` `Algebra.instIsStandardOpenImmersionTensorProduct`
`of_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`RingHom.IsStandardOpenImmersion`	—	`IsLocalization.away_of_isUnit_of_bijective` `isUnit_one`
`respectsIso` 📖	mathematical	—	`RingHom.RespectsIso` `RingHom.IsStandardOpenImmersion`	—	`RingHom.StableUnderComposition.respectsIso` `stableUnderComposition` `of_bijective` `RingEquiv.bijective`
`stableUnderComposition` 📖	mathematical	—	`RingHom.StableUnderComposition` `RingHom.IsStandardOpenImmersion`	—	`comp`
`toAlgebra` 📖	mathematical	—	`Algebra.IsStandardOpenImmersion` `CommRing.toCommSemiring` `RingHom.toAlgebra`	—	—

---

← Back to Index