All.lean
Nyll.SchemeTheory.RingTheory.All
0 declarations indexed from sourceView source ↗
Module documentation
Ring-theoretic foundations for scheme constructions
This aggregate exposes adic completions, generic fibres, henselian factorizations, flatness and descent, normalization, and ramification modules.
Imports102
- Nyll.SchemeTheory.RingTheory.AdicCompletion.All
- Nyll.SchemeTheory.RingTheory.CyclicIdempotentAnnihilator
- Nyll.SchemeTheory.RingTheory.CyclicIdempotentFactor
- Nyll.SchemeTheory.RingTheory.Descent.All
- Nyll.SchemeTheory.RingTheory.DepthTwoRegularPair
- Nyll.SchemeTheory.RingTheory.RegularLocalQuotientLift
- Nyll.SchemeTheory.RingTheory.RegularLocalDimensionOne
- Nyll.SchemeTheory.RingTheory.ReducedCartierDivisor
- Nyll.SchemeTheory.RingTheory.PuncturedHypersurfacePrime
- Nyll.SchemeTheory.RingTheory.DeterminantTrickCongruence
- Nyll.SchemeTheory.RingTheory.FiniteOpenFactor
- Nyll.SchemeTheory.RingTheory.GenericFiber.All
- Nyll.SchemeTheory.RingTheory.HenselianCyclicIdempotent
- Nyll.SchemeTheory.RingTheory.HenselianFactorization
- Nyll.SchemeTheory.RingTheory.HenselianFiniteIdempotent
- Nyll.SchemeTheory.RingTheory.HenselianIdempotents
- Nyll.SchemeTheory.RingTheory.HenselianIntegral
- Nyll.SchemeTheory.RingTheory.HenselianIntegralCyclicIdempotent
- Nyll.SchemeTheory.RingTheory.HenselianNilIdeal
- Nyll.SchemeTheory.RingTheory.IdempotentAnnihilator
- Nyll.SchemeTheory.RingTheory.IdempotentFactorReduction
- Nyll.SchemeTheory.RingTheory.IdempotentFromCoprimeFactors
- Nyll.SchemeTheory.RingTheory.IdempotentLiftSupport
- Nyll.SchemeTheory.RingTheory.IdempotentLocalizationCyclicity
- Nyll.SchemeTheory.RingTheory.IdempotentQuotientFactor
- Nyll.SchemeTheory.RingTheory.IntegralLocalizationFiniteModel
- Nyll.SchemeTheory.RingTheory.IntegralLocalizationIdempotentModel
- Nyll.SchemeTheory.RingTheory.JacobianLocalization
- Nyll.SchemeTheory.RingTheory.JacobsonIdempotentFactor
- Nyll.SchemeTheory.RingTheory.JacobsonIdempotentRigidity
- Nyll.SchemeTheory.RingTheory.JacobsonIntegral
- Nyll.SchemeTheory.RingTheory.Localization.All
- Nyll.SchemeTheory.RingTheory.LocalizationIdempotentFactor
- Nyll.SchemeTheory.RingTheory.OpenImmersionFiniteFactor
- Nyll.SchemeTheory.RingTheory.QuotientBaseChange
- Nyll.SchemeTheory.RingTheory.Ramification.All
- Nyll.SchemeTheory.RingTheory.SmoothReduced
- Nyll.SchemeTheory.RingTheory.TensorProductPrime
- Nyll.SchemeTheory.RingTheory.FiniteProductFaithfullyFlat
- Nyll.SchemeTheory.RingTheory.SeparableConstantsTensor
- Nyll.SchemeTheory.RingTheory.FractionFieldSubalgebraTrace
- Nyll.SchemeTheory.RingTheory.RegularLocalFiniteFreeResolution
- Nyll.SchemeTheory.RingTheory.RegularLocalTrace
- Nyll.SchemeTheory.RingTheory.FractionFieldTensorDomain
- Nyll.SchemeTheory.RingTheory.FiniteResidueGeometricPoint
- Nyll.SchemeTheory.RingTheory.DVRFractionFieldAway
- Nyll.SchemeTheory.RingTheory.HenselianFiniteDomainLocal
- Nyll.SchemeTheory.RingTheory.StrictHenselianFiniteDomainPoint
- Nyll.SchemeTheory.RingTheory.IntegralClosureSplitProduct
- Nyll.SchemeTheory.RingTheory.IntegralClosureEtaleOfSplit
- Nyll.SchemeTheory.RingTheory.LocalizationTensorTower
- Nyll.SchemeTheory.RingTheory.StrictHenselianFiniteDomainPointLift
- Nyll.SchemeTheory.RingTheory.Flat.All
- Nyll.SchemeTheory.RingTheory.LocalAlgebra
- Nyll.SchemeTheory.RingTheory.CohenMacaulay
- Nyll.SchemeTheory.RingTheory.FreeModuleRegularScalar
- Nyll.SchemeTheory.RingTheory.FreeModuleRegularSequenceAux
- Nyll.SchemeTheory.RingTheory.FreeModuleRegularSequence
- Nyll.SchemeTheory.RingTheory.ModuleDepthBound
- Nyll.SchemeTheory.RingTheory.ModuleDepthRegularQuotient
- Nyll.SchemeTheory.RingTheory.CommonRegularElement
- Nyll.SchemeTheory.RingTheory.RegularLocalDepth
- Nyll.SchemeTheory.RingTheory.RegularLocalDepthFreeness
- Nyll.SchemeTheory.RingTheory.RegularLocalDomain
- Nyll.SchemeTheory.RingTheory.HomogeneousIdealMap
- Nyll.SchemeTheory.RingTheory.EtaleFieldPointBound
- Nyll.SchemeTheory.RingTheory.EtaleFieldPointGlobalBound
- Nyll.SchemeTheory.RingTheory.FinitePresentationAwayRelations
- Nyll.SchemeTheory.RingTheory.FinitePresentationCoequalizer
- Nyll.SchemeTheory.RingTheory.IntegralFinitePresentationColimit
- Nyll.SchemeTheory.RingTheory.IntegralFinitePresentationDiagram
- Nyll.SchemeTheory.RingTheory.IntegralFinitePresentationModel
- Nyll.SchemeTheory.RingTheory.ModuleFiniteLocalizationModel
- Nyll.SchemeTheory.RingTheory.ModuleKernelLocalization
- Nyll.SchemeTheory.RingTheory.GenericTensorSplit
- Nyll.SchemeTheory.RingTheory.SignPolynomialAction
- Nyll.SchemeTheory.RingTheory.SignPolynomialMonomials
- Nyll.SchemeTheory.RingTheory.SignPolynomialInvariants
- Nyll.SchemeTheory.RingTheory.SignPolynomialFinite
- Nyll.SchemeTheory.RingTheory.SignPolynomialNormal
- Nyll.SchemeTheory.RingTheory.SignPolynomialDegree
- Nyll.SchemeTheory.RingTheory.HenselianIntegralDomainLocal
- Nyll.SchemeTheory.RingTheory.HenselianIntegralClosureUnits
- Nyll.SchemeTheory.RingTheory.HenselianOrthogonalIdempotents
- Nyll.SchemeTheory.RingTheory.OrthogonalIdempotentsDegree
- Nyll.SchemeTheory.RingTheory.StrictHenselianFiberDegree
- Nyll.SchemeTheory.RingTheory.IntegralPurelyInseparableLocalTensor
- Nyll.SchemeTheory.RingTheory.FlatTensorNilpotentKernel
- Nyll.SchemeTheory.RingTheory.GeometricallyUnibranch
- Nyll.SchemeTheory.RingTheory.SubmoduleAdjoinLocalization
- Nyll.SchemeTheory.RingTheory.SubmoduleAdjoinRestriction
- Nyll.SchemeTheory.RingTheory.LocalizedSubmoduleComparison
- Nyll.SchemeTheory.RingTheory.SubalgebraResidueFieldColimit
- Nyll.SchemeTheory.RingTheory.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
- Nyll.SchemeTheory.RingTheory.HenselianLocalRing_exists_algHom_lift_of_etale
- Nyll.SchemeTheory.RingTheory.HenselianLocalRing_exists_completeOrthogonalIdempotents_forall_isLocalRing_quotient_of_moduleFinite
- Nyll.SchemeTheory.RingTheory.HenselianLocalRing_of_isIntegral_of_isLocalRing
- Nyll.SchemeTheory.RingTheory.HenselianLocalRing_of_moduleFinite_of_isLocalRing
- Nyll.SchemeTheory.RingTheory.Module_Finite_of_ker_le_range_of_isNoetherianRing
- Nyll.SchemeTheory.RingTheory.NonfiniteGeneratorCount
- Nyll.SchemeTheory.RingTheory.PrimeContainingAtHeightOne
- Nyll.SchemeTheory.RingTheory.NormPolynomial
Imported by1
This module has no indexed declarations. Its imports and full source are available here.