Documentation Verification Report

Fiber

📁 Source: Mathlib/RingTheory/Smooth/Fiber.lean

Statistics

Metric	Count
Definitions `Fiber`, `Fiber`, `Fiber`, `Fiber`	4
Theorems `of_formallyUnramified_of_flat`, `of_formallySmooth_residueField_tensor`, `of_isUnramifiedAt_of_flat`, `of_formallySmooth_fiber`, `of_formallySmooth_fiber`	5
Total	9

Algebra.Etale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_formallyUnramified_of_flat` 📖	mathematical	—	`Algebra.Etale`	—	`Algebra.Smooth.of_formallySmooth_fiber` `Algebra.to_smulCommClass` `Algebra.FormallyEtale.instFormallySmooth` `Localization.AtPrime.isLocalRing` `Algebra.FormallyEtale.of_formallyUnramified_of_field` `Algebra.EssFiniteType.baseChange` `Algebra.EssFiniteType.of_finiteType` `Algebra.FiniteType.of_finitePresentation` `Algebra.FormallyUnramified.base_change` `Algebra.FormallyUnramified.subsingleton_kaehlerDifferential` `Algebra.FormallySmooth.subsingleton_h1Cotangent` `Algebra.Smooth.formallySmooth`

Algebra.FormallySmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_formallySmooth_residueField_tensor` 📖	mathematical	—	`Algebra.FormallySmooth`	—	`Algebra.to_smulCommClass` `Algebra.FiniteType.iff_quotient_mvPolynomial''` `Algebra.FiniteType.of_finitePresentation` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization` `IsLocalization.map_units` `IsLocalization.exists_mk'_eq` `Submonoid.instSubmonoidClass` `IsLocalization.lift_mk'` `Units.coe_liftRight` `RingHom.instRingHomClass` `Algebra.FinitePresentation.ker_fG_of_surjective` `Algebra.FinitePresentation.mvPolynomial` `Algebra.FinitePresentation.self` `Finite.of_fintype` `le_antisymm` `IsLocalization.map_eq_zero_iff` `IsLocalization.mk'_mem_map_algebraMap_iff` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `Ideal.map_le_iff_le_comap` `IsLocalization.lift_eq` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `Ideal.FG.map` `Algebra.FormallyEtale.of_isLocalization` `comp` `Algebra.mvPolynomial` `instLocalization` `inst` `Module.Free.of_equiv` `Algebra.TensorProduct.instFree` `instFreeMvPolynomialKaehlerDifferential` `IsScalarTower.of_algHom` `KaehlerDifferential.finite` `Algebra.instEssFiniteTypeLocalization` `Algebra.EssFiniteType.of_finiteType` `Algebra.FiniteType.instMvPolynomialOfFinite`

Algebra.IsEtaleAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isUnramifiedAt_of_flat` 📖	mathematical	—	`Algebra.IsEtaleAt`	—	`Algebra.exists_unramified_of_isUnramifiedAt` `Algebra.FiniteType.of_finitePresentation` `Algebra.Etale.of_formallyUnramified_of_flat` `instFinitePresentationAway` `Localization.flat` `Algebra.Unramified.formallyUnramified` `Algebra.basicOpen_subset_etaleLocus_iff` `Algebra.Etale.formallyEtale`

Algebra.IsSmoothAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_formallySmooth_fiber` 📖	mathematical	—	`Algebra.IsSmoothAt`	—	`Algebra.to_smulCommClass` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization` `AlgHom.map_algebraMap` `IsLocalization.map_units` `Ideal.over_def` `Ideal.primeCompl.congr_simp` `IsScalarTower.to₁₃₄` `IsScalarTower.of_algHom` `IsScalarTower.of_algebraMap_eq'` `IsLocalization.ringHom_ext` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `instIsScalarTowerLocalizationAlgebraMapSubmonoid` `IsLocalization.isLocalization_of_submonoid_le` `Algebra.IsPushout.symm` `Algebra.isPushout_of_isLocalization` `Algebra.FinitePresentation.equiv` `Algebra.FinitePresentation.baseChange` `Localization.AtPrime.isLocalRing` `Algebra.TensorProduct.instSMulCommClassTensorProduct_1` `Algebra.FormallySmooth.comp` `TensorProduct.isScalarTower_left` `Algebra.FormallySmooth.instTensorProduct` `Algebra.FormallySmooth.instLocalization` `Algebra.FormallySmooth.inst` `AlgEquiv.map_mul'` `AlgEquiv.map_add'` `IsScalarTower.to_smulCommClass'` `Algebra.TensorProduct.right_isScalarTower` `IsLocalRing.instIsScalarTowerResidueField` `OreLocalization.instSMulCommClass` `TensorProduct.isScalarTower` `IsScalarTower.to_smulCommClass` `TensorProduct.CompatibleSMul.isScalarTower` `IsLocalization.instCompatibleSMulLocalizationOfIsScalarTower_1` `Ideal.ResidueField.algHom_ext` `Algebra.ext_id` `Algebra.FormallySmooth.of_equiv` `Algebra.FormallySmooth.of_formallySmooth_residueField_tensor` `instFlatAtPrime` `instIsLocalHomAtPrimeRingHomAlgebraMap`

Algebra.Smooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_formallySmooth_fiber` 📖	mathematical	`Algebra.FormallySmooth` `Ideal.ResidueField` `Ideal.Fiber` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Algebra.TensorProduct.instCommRing` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id` `Algebra.TensorProduct.leftAlgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Algebra.to_smulCommClass` `IsLocalRing.ResidueField`	`Algebra.Smooth`	—	`Algebra.to_smulCommClass` `Algebra.smoothLocus_eq_univ_iff` `Set.eq_univ_iff_forall` `Algebra.IsSmoothAt.of_formallySmooth_fiber` `Ideal.IsPrime.under` `PrimeSpectrum.isPrime` `Ideal.over_under`

FiberBundleCore

Definitions

Name	Category	Theorems
`Fiber` 📖	CompOp	13 math math: `mk_mem_localTrivAt_source`, `mem_localTrivAt_source`, `mem_localTrivAsPartialEquiv_source`, `localTriv_apply`, `mem_localTriv_source`, `localTrivAt_apply`, `localTrivAsPartialEquiv_apply`, `mem_localTrivAt_target`, `mem_localTrivAt_baseSet`, `localTrivAt_apply_mk`, `continuous_totalSpaceMk`, `localTriv_symm_apply`, `localTrivAt_snd`

Function

Definitions

Name	Category	Theorems
`Fiber` 📖	CompOp	5 math math: `TopologicalSpace.Fiber.sigmaIsoHom_inj`, `TopologicalSpace.Fiber.sigmaIsoHom_apply`, `TopologicalSpace.Fiber.instFiniteFiberCoeLocallyConstant`, `TopologicalSpace.Fiber.sigmaIsoHom_surj`, `CompHausLike.LocallyConstant.sigmaComparison_comp_sigmaIso`

Ideal

Definitions

Name	Category	Theorems
`Fiber` 📖	CompOp	13 math math: `PrimeSpectrum.preimageEquivFiber_symm_apply_coe`, `Polynomial.fiberEquivQuotient_tmul`, `instLiesOverFiberOfIsPrime`, `PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal`, `PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal`, `PrimeSpectrum.preimageEquivFiber_apply_asIdeal`, `Algebra.QuasiFinite.finite_fiber`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal`, `PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal`, `PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe`, `Algebra.QuasiFinite.instIsArtinianRingFiber`, `Fiber.exists_smul_eq_one_tmul`

VectorBundleCore

Definitions

Name	Category	Theorems
`Fiber` 📖	CompOp	17 math math: `mem_localTriv_target`, `continuous_proj`, `localTriv_symm_fst`, `localTrivAt_apply`, `isOpenMap_proj`, `baseSet_at`, `mem_source_at`, `instContMDiffVectorBundle`, `localTriv_apply`, `localTrivAt_apply_mk`, `tangentBundleCore_localTriv_baseSet`, `inCoordinates_eq`, `trivializationAt`, `mem_localTriv_source`, `localTriv.isLinear`, `mem_localTrivAt_baseSet`, `vectorBundle`

---

← Back to Index