Instances on residue fields

instance instIsSeparableResidueFieldOfQuotientIdeal {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (q : Ideal B) [q.LiesOver p] [p.IsMaximal] [q.IsMaximal] [Algebra (Localization.AtPrime p) (Localization.AtPrime q)] [IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime q)] [Algebra.IsSeparable (A ⧸ p) (B ⧸ q)] : Algebra.IsSeparable p.ResidueField q.ResidueField

instance instIsSeparableQuotientIdealOfResidueField {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (q : Ideal B) [q.LiesOver p] [p.IsMaximal] [q.IsMaximal] [Algebra (Localization.AtPrime p) (Localization.AtPrime q)] [IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime q)] [Algebra.IsSeparable p.ResidueField q.ResidueField] : Algebra.IsSeparable (A ⧸ p) (B ⧸ q)

theorem Algebra.isSeparable_residueField_iff {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} {q : Ideal B} [q.LiesOver p] [p.IsMaximal] [q.IsMaximal] [Algebra (Localization.AtPrime p) (Localization.AtPrime q)] [IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime q)] : Algebra.IsSeparable p.ResidueField q.ResidueField ↔ Algebra.IsSeparable (A ⧸ p) (B ⧸ q)

instance instIsAlgebraicQuotientIdealResidueField {A : Type u_2} [CommRing A] (p : Ideal A) [p.IsPrime] : Algebra.IsAlgebraic (A ⧸ p) p.ResidueField

instance instIsAlgebraicResidueFieldOfIsIntegral {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (q : Ideal B) [q.LiesOver p] [p.IsPrime] [q.IsPrime] [Algebra (Localization.AtPrime p) (Localization.AtPrime q)] [IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime q)] [Algebra.IsIntegral A B] : Algebra.IsAlgebraic p.ResidueField q.ResidueField

@[instance_reducible]

instance IsLocalRing.ResidueField.algebraOfIsIntegral {R : Type u_4} {k : Type u_5} [CommRing R] [IsLocalRing R] [Field k] [Algebra R k] [Algebra.IsIntegral R k] : Algebra (ResidueField R) k

Equations

• One or more equations did not get rendered due to their size.

instance IsLocalRing.ResidueField.isScalarTowerOfIsIntegral {R : Type u_4} {k : Type u_5} [CommRing R] [IsLocalRing R] [Field k] [Algebra R k] [Algebra.IsIntegral R k] : IsScalarTower R (ResidueField R) k

instance IsLocalRing.instFiniteResidueField_1 {R : Type u_4} {k : Type u_5} [CommRing R] [IsLocalRing R] [Field k] [Algebra R k] [Module.Finite R k] : Module.Finite (ResidueField R) k