Local Ring Properties of Equalizers and Pullbacks

In this file we provide basic lemmas for the equalizers the pullbacks and of ring homomorphisms and algebra homomorphisms. We show that they preserve the property of being a local ring under suitable conditions.

Main definitions

• RingHom.pullback: The pullback of two ring homomorphisms f : R →+* T and g : S →+* T, defined as the subring of R × S consisting of pairs (r, s) such that f r = g s.

• RingHom.pullbackFst, RingHom.pullbackSnd: The canonical projection maps from the pullback to R and S.

Main results

• RingHom.isLocalRing_eqLocus: The equalizer of two ring homomorphisms from a local ring is again a local ring.

• RingHom.isLocalRing_pullback: The pullback of f : R →+* T and g : S →+* T is a local ring, provided that R is a local ring and g is a local homomorphism.

theorem RingHom.isLocalRing_eqLocus {R : Type u_1} {T : Type u_3} [Ring R] [Semiring T] [IsLocalRing R] (f g : R →+* T) : IsLocalRing ↥(f.eqLocus g)

@[reducible, inline]

abbrev RingHom.pullback {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Semiring T] (f : R →+* T) (g : S →+* T) : Subring (R × S)

The subring of pairs (r, s) : R × S such that f r = g s, i.e., the pullback of f : R →+* T and g : S →+* T as a subring of R × S.

Equations

• f.pullback g = (f.comp (RingHom.fst R S)).eqLocus (g.comp (RingHom.snd R S))

@[reducible, inline]

abbrev RingHom.pullbackFst {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Semiring T] (f : R →+* T) (g : S →+* T) : ↥(f.pullback g) →+* R

The first projection from the pullback of f : R →+* T and g : S →+* T to R.

Equations

• f.pullbackFst g = (RingHom.fst R S).comp (f.pullback g).subtype

@[reducible, inline]

abbrev RingHom.pullbackSnd {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Semiring T] (f : R →+* T) (g : S →+* T) : ↥(f.pullback g) →+* S

The second projection from the pullback of f : R →+* T and g : S →+* T to S.

Equations

• f.pullbackSnd g = (RingHom.snd R S).comp (f.pullback g).subtype

theorem RingHom.pullback_comm_sq {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Semiring T] (f : R →+* T) (g : S →+* T) : f.comp (f.pullbackFst g) = g.comp (f.pullbackSnd g)

theorem RingHom.isUnit_pullback_mk_iff {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Semiring T] (f : R →+* T) (g : S →+* T) {a : R × S} (a_in : a ∈ f.pullback g) : IsUnit ⟨a, a_in⟩ ↔ IsUnit a.1 ∧ IsUnit a.2

instance RingHom.isLocalHom_pullbackFst {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Semiring T] (f : R →+* T) (g : S →+* T) [IsLocalHom g] : IsLocalHom (f.pullbackFst g)

instance RingHom.isLocalHom_pullbackSnd {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Semiring T] (f : R →+* T) (g : S →+* T) [IsLocalHom f] : IsLocalHom (f.pullbackSnd g)

theorem RingHom.surjective_pullbackFst_of_surjective {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Semiring T] (f : R →+* T) (g : S →+* T) (h : Function.Surjective ⇑g) : Function.Surjective ⇑(f.pullbackFst g)

theorem RingHom.surjective_pullbackSnd_of_surjective {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Semiring T] (f : R →+* T) (g : S →+* T) (h : Function.Surjective ⇑f) : Function.Surjective ⇑(f.pullbackSnd g)

theorem RingHom.map_pullbackSnd_ker_pullbackFst_eq {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Semiring T] (f : R →+* T) (g : S →+* T) : Ideal.map (f.pullbackSnd g) (ker (f.pullbackFst g)) = ker g

theorem RingHom.isLocalRing_pullback {R : Type u_1} {S : Type u_2} {T : Type u_3} [Ring R] [Ring S] [Semiring T] [IsLocalRing R] (f : R →+* T) (g : S →+* T) [IsLocalHom g] : IsLocalRing ↥(f.pullback g)

@[reducible, inline]

abbrev AlgHom.pullback {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) : Subalgebra R (A × B)

The subalgebra of pairs (a, b) : A × B such that f a = g b, i.e., the pullback of f and g as a subalgebra of A × B.

Equations

• f.pullback g = (f.comp (AlgHom.fst R A B)).equalizer (g.comp (AlgHom.snd R A B))

@[reducible, inline]

abbrev AlgHom.pullbackFst {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) : ↥(f.pullback g) →ₐ[R] A

The first projection from the pullback of f and g to A.

Equations

• f.pullbackFst g = (AlgHom.fst R A B).comp (f.pullback g).val

@[reducible, inline]

abbrev AlgHom.pullbackSnd {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) : ↥(f.pullback g) →ₐ[R] B

The second projection from the pullback of f and g to B.

Equations

• f.pullbackSnd g = (AlgHom.snd R A B).comp (f.pullback g).val

theorem AlgHom.pullback_comm_sq {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) : f.comp (f.pullbackFst g) = g.comp (f.pullbackSnd g)

theorem AlgHom.isUnit_pullback_mk_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) {a : A × B} (a_in : a ∈ f.pullback g) : IsUnit ⟨a, a_in⟩ ↔ IsUnit a.1 ∧ IsUnit a.2

theorem AlgHom.surjective_pullbackFst_of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (h : Function.Surjective ⇑g) : Function.Surjective ⇑(f.pullbackFst g)

theorem AlgHom.surjective_pullbackSnd_of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (h : Function.Surjective ⇑f) : Function.Surjective ⇑(f.pullbackSnd g)

theorem AlgHom.isLocalRing_pullback {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] [Semiring C] [Algebra R C] [IsLocalRing A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) [IsLocalHom g] : IsLocalRing ↥(f.pullback g)