Documentation Verification Report

LocalIso

📁 Source: Mathlib/AlgebraicGeometry/Morphisms/LocalIso.lean

Statistics

Metric	Count
Definitions `IsLocalIso`	1
Theorems `eq_iInf`, `eq_sourceLocalClosure_isOpenImmersion`, `exists_isOpenImmersion`, `instIsMultiplicativeScheme`, `instIsStableUnderBaseChangeScheme`, `instIsZariskiLocalAtSource`, `le_of_isLocalAtSource`, `le_of_isZariskiLocalAtSource`, `isLocalIso_iff`	9
Total	10

AlgebraicGeometry

Definitions

Name	Category	Theorems
`IsLocalIso` 📖	CompData	8 math math: `IsLocalIso.le_of_isZariskiLocalAtSource`, `IsLocalIso.instIsZariskiLocalAtSource`, `IsLocalIso.eq_iInf`, `IsLocalIso.le_of_isLocalAtSource`, `IsLocalIso.instIsStableUnderBaseChangeScheme`, `isLocalIso_iff`, `IsLocalIso.instIsMultiplicativeScheme`, `IsLocalIso.eq_sourceLocalClosure_isOpenImmersion`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalIso_iff` 📖	mathematical	—	`IsLocalIso` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `IsOpenImmersion` `Scheme.Opens.toScheme` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Scheme.Opens.ι`	—	—

AlgebraicGeometry.IsLocalIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_iInf` 📖	mathematical	—	`AlgebraicGeometry.IsLocalIso` `iInf` `CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.ContainsIdentities` `AlgebraicGeometry.IsZariskiLocalAtSource`	—	`le_antisymm` `le_of_isZariskiLocalAtSource` `iInf_le_of_le` `CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities` `instIsMultiplicativeScheme` `iInf_le` `instIsZariskiLocalAtSource`
`eq_sourceLocalClosure_isOpenImmersion` 📖	mathematical	—	`AlgebraicGeometry.IsLocalIso` `AlgebraicGeometry.sourceLocalClosure` `AlgebraicGeometry.IsOpenImmersion`	—	`AlgebraicGeometry.isLocalIso_iff` `AlgebraicGeometry.sourceLocalClosure.iff_forall_exists` `AlgebraicGeometry.isOpenImmersion_respectsIso`
`exists_isOpenImmersion` 📖	mathematical	—	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `AlgebraicGeometry.IsOpenImmersion` `AlgebraicGeometry.Scheme.Opens.toScheme` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Opens.ι`	—	—
`instIsMultiplicativeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsLocalIso`	—	`eq_sourceLocalClosure_isOpenImmersion` `AlgebraicGeometry.sourceLocalClosure.instIsMultiplicativeSchemeOfIsStableUnderBaseChange` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_isMultiplicative`
`instIsStableUnderBaseChangeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsLocalIso`	—	`eq_sourceLocalClosure_isOpenImmersion` `AlgebraicGeometry.sourceLocalClosure.instIsStableUnderBaseChangeScheme` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion`
`instIsZariskiLocalAtSource` 📖	mathematical	—	`AlgebraicGeometry.IsZariskiLocalAtSource` `AlgebraicGeometry.IsLocalIso`	—	`eq_sourceLocalClosure_isOpenImmersion` `AlgebraicGeometry.sourceLocalClosure.instIsZariskiLocalAtSourceIsOpenImmersionOfRespectsIsoOfRespectsLeftScheme` `AlgebraicGeometry.isOpenImmersion_respectsIso` `CategoryTheory.MorphismProperty.Respects.toRespectsLeft` `CategoryTheory.MorphismProperty.instRespectsOfIsStableUnderComposition` `AlgebraicGeometry.isOpenImmersion_isStableUnderComposition`
`le_of_isLocalAtSource` 📖	mathematical	—	`Pi.hasLe` `AlgebraicGeometry.Scheme` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `Prop.le` `AlgebraicGeometry.IsLocalIso`	—	`le_of_isZariskiLocalAtSource`
`le_of_isZariskiLocalAtSource` 📖	mathematical	—	`Pi.hasLe` `AlgebraicGeometry.Scheme` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `Prop.le` `AlgebraicGeometry.IsLocalIso`	—	`eq_sourceLocalClosure_isOpenImmersion` `AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover` `AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion`

---

← Back to Index