Structures · Algebra
Localization.AtPrime.IsLiesOverAlgebra
A predicate expressing that Localization.AtPrime P is an algebra over Localization.AtPrime p
in the natural way when P lies over p.
- Shape
- 2 explicit arguments · adds algebraMap_eq
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by40
- Ideal.inertiaDeg_eq
- Polynomial.residueFieldMapCAlgEquiv
- Ideal.inertiaDeg_def
- Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq
- Algebra.isUnramifiedAt_iff_map_eq
- Localization.localAlgEquiv'
- Ideal.Fiber.localizationAlgEquivQuotient
- Ideal.ramificationIdx_tower'
- Polynomial.residueFieldMapCAlgEquiv_algebraMap
- Localization.localAlgHom'
- Algebra.WeaklyQuasiFiniteAt.finite_residueField
- Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top
- Localization.localRingHom_surjective_of_primesOver_eq_singleton
- Ideal.residueFieldAlgEquiv'
- Localization.finite_of_primesOver_eq_singleton
- Ideal.Fiber.lift_residueField_surjective
- Polynomial.residueFieldMapCAlgEquiv_symm_C
- Algebra.instIsSeparableResidueFieldOfIsUnramifiedAt
- Algebra.isSeparable_residueField_iff
- Polynomial.residueFieldMapCAlgEquiv_symm_X
- instIsAlgebraicResidueFieldOfIsIntegral
- Ideal.ramificationIdx'_tower'
- Algebra.QuasiFinite.instFiniteResidueField
- Localization.localAlgEquiv'_symm_apply
- Ideal.inertiaDeg'_def
- Localization.localAlgHom'_apply
- instIsSeparableResidueFieldOfQuotientIdeal
- Polynomial.residueFieldMapCAlgEquiv.congr_simp
- instEssFiniteTypeResidueField_1
- Algebra.instFiniteResidueFieldOfIsUnramifiedAt
- instIsSeparableQuotientIdealOfResidueField
- Localization.localAlgEquiv'_apply
- Localization.AtPrime.instIsScalarTowerOfIsLiesOverAlgebra
- Algebra.instFormallyUnramifiedAtPrimeOfIsUnramifiedAtOfIsLiesOverAlgebra
- Algebra.instFiniteResidueFieldOfQuasiFiniteAt
- Ideal.inertiaDeg'_eq
- Localization.exists_awayMap_bijective_of_residueField_surjective
- instFlatAtPrimeOfIsLiesOverAlgebra
- instIsLocalHomAtPrimeRingHomAlgebraMap
- Localization.AtPrime.instIsScalarTowerOfIsLiesOverAlgebra_1
Ancestors0
No ancestors.