class IsResidueAlgebra (𝓞 : Type u_1) [CommRing 𝓞] (A : Type u_2) [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] : Prop

IsResidueAlgebra 𝓞 indicates that A [Algebra 𝓞 A] has the same residue field as 𝓞. It is sufficient for the natural map 𝓞 to 𝓴 A to be surjective. The actual ≃+* between residue fields is given in IsResidueAlgebra.ringEquiv.

• isSurjective' : Function.Surjective ⇑(algebraMap 𝓞 (IsLocalRing.ResidueField A))

theorem IsResidueAlgebra.isSurjective (𝓞 : Type u_1) [CommRing 𝓞] (A : Type u_2) [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] : Function.Surjective ⇑(algebraMap 𝓞 (IsLocalRing.ResidueField A))

theorem IsResidueAlgebra.algebraMap_surjective (𝓞 : Type u_1) [CommRing 𝓞] (A : Type u_2) [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] : Function.Surjective ⇑(algebraMap 𝓞 (IsLocalRing.ResidueField A))

instance IsResidueAlgebra.inst (𝓞 : Type u_1) [CommRing 𝓞] [IsLocalRing 𝓞] : IsResidueAlgebra 𝓞 𝓞

instance IsResidueAlgebra.instIsLocalHomRingHomAlgebraMapOfIsLocalRing (𝓞 : Type u_1) [CommRing 𝓞] (A : Type u_2) [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] [IsLocalRing 𝓞] : IsLocalHom (algebraMap 𝓞 A)

theorem IsResidueAlgebra.surjective (𝓞 : Type u_1) [CommRing 𝓞] (A : Type u_2) [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] [IsLocalRing 𝓞] : Function.Surjective ⇑(algebraMap (IsLocalRing.ResidueField 𝓞) (IsLocalRing.ResidueField A))

theorem IsResidueAlgebra.algebraMap_bijective (𝓞 : Type u_1) [CommRing 𝓞] (A : Type u_2) [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] [IsLocalRing 𝓞] : Function.Bijective ⇑(algebraMap (IsLocalRing.ResidueField 𝓞) (IsLocalRing.ResidueField A))

noncomputable def IsResidueAlgebra.ringEquiv (𝓞 : Type u_1) [CommRing 𝓞] (A : Type u_2) [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] [IsLocalRing 𝓞] : IsLocalRing.ResidueField 𝓞 ≃+* IsLocalRing.ResidueField A

Ring equivalence between the residue field of 𝓞 and A, when [IsResidueAlgebra 𝓞 A]

Equations

• IsResidueAlgebra.ringEquiv 𝓞 A = RingEquiv.ofBijective (algebraMap (IsLocalRing.ResidueField 𝓞) (IsLocalRing.ResidueField A)) ⋯

noncomputable def IsResidueAlgebra.algEquiv (𝓞 : Type u_1) [CommRing 𝓞] (A : Type u_2) [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] [IsLocalRing 𝓞] : IsLocalRing.ResidueField 𝓞 ≃ₐ[𝓞] IsLocalRing.ResidueField A

Equations

• IsResidueAlgebra.algEquiv 𝓞 A = { toEquiv := (IsResidueAlgebra.ringEquiv 𝓞 A).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem IsResidueAlgebra.of_localHom {𝓞 : Type u_1} [CommRing 𝓞] {A : Type u_2} [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] {B : Type u_3} [CommRing B] [Algebra 𝓞 B] [IsLocalRing B] (f : B →ₐ[𝓞] A) [IsLocalHom f] [IsResidueAlgebra 𝓞 A] : IsResidueAlgebra 𝓞 B

theorem IsResidueAlgebra.Ideal.neq_top_of_nontrivial_quotient {A : Type u_2} [CommRing A] (I : Ideal A) [nontrivial : Nontrivial (A ⧸ I)] : I ≠ ⊤

theorem IsResidueAlgebra.residue_of_quot_surjective {A : Type u_2} [CommRing A] [IsLocalRing A] (I : Ideal A) [Nontrivial (A ⧸ I)] : Function.Surjective ⇑(algebraMap (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField (A ⧸ I)))

instance IsResidueAlgebra.quotient (𝓞 : Type u_1) [CommRing 𝓞] (A : Type u_2) [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] (I : Ideal A) [Nontrivial (A ⧸ I)] : IsResidueAlgebra 𝓞 (A ⧸ I)

instance IsResidueAlgebra.instResidueField (𝓞 : Type u_1) [CommRing 𝓞] (A : Type u_2) [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] : IsResidueAlgebra 𝓞 (IsLocalRing.ResidueField A)

theorem IsResidueAlgebra.of_restrictScalars {𝓞 : Type u_1} [CommRing 𝓞] {A : Type u_2} [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] {B : Type u_4} [CommRing B] [Algebra 𝓞 B] [IsLocalRing B] [IsResidueAlgebra 𝓞 B] [Algebra A B] [isScalarTower : IsScalarTower 𝓞 A B] [isLocalHom : IsLocalHom (algebraMap A B)] : IsResidueAlgebra A B

theorem IsResidueAlgebra.exists_sub_mem_maximalIdeal (𝓞 : Type u_1) [CommRing 𝓞] {A : Type u_2} [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] (r : A) : ∃ (a : 𝓞), r - (algebraMap 𝓞 A) a ∈ IsLocalRing.maximalIdeal A

noncomputable def IsResidueAlgebra.preimage (𝓞 : Type u_1) [CommRing 𝓞] {A : Type u_2} [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] (r : A) : 𝓞

For an r : A, this is an arbitrary choice of x : 𝓞 such that r ≡ x (mod 𝔪_A).

Equations

• IsResidueAlgebra.preimage 𝓞 r = ⋯.choose

theorem IsResidueAlgebra.preimage_spec (𝓞 : Type u_1) [CommRing 𝓞] {A : Type u_2} [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] (r : A) : r - (algebraMap 𝓞 A) (preimage 𝓞 r) ∈ IsLocalRing.maximalIdeal A

theorem IsResidueAlgebra.residue_preimage (𝓞 : Type u_1) [CommRing 𝓞] {A : Type u_2} [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] (r : A) : (IsLocalRing.residue A) ((algebraMap 𝓞 A) (preimage 𝓞 r)) = (IsLocalRing.residue A) r

theorem IsResidueAlgebra.residue_preimage_eq_iff (𝓞 : Type u_1) [CommRing 𝓞] {A : Type u_2} [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] [IsLocalRing 𝓞] [IsLocalHom (algebraMap 𝓞 A)] {r : A} {a : IsLocalRing.ResidueField 𝓞} : (IsLocalRing.residue 𝓞) (preimage 𝓞 r) = a ↔ (IsLocalRing.residue A) r = (IsLocalRing.ResidueField.map (algebraMap 𝓞 A)) a

theorem IsResidueAlgebra.residue_preimage_map (𝓞 : Type u_1) [CommRing 𝓞] {A : Type u_2} [CommRing A] [Algebra 𝓞 A] [IsLocalRing A] [IsResidueAlgebra 𝓞 A] [IsLocalRing 𝓞] [IsLocalHom (algebraMap 𝓞 A)] {B : Type u_3} [CommRing B] [Algebra 𝓞 B] [IsLocalRing B] [IsResidueAlgebra 𝓞 B] (f : A →ₐ[𝓞] B) [IsLocalHom f] (x : A) : (IsLocalRing.residue 𝓞) (preimage 𝓞 x) = (IsLocalRing.residue 𝓞) (preimage 𝓞 (f x))