Properties of P.Under ⊤ R for R : CommRingCat

In this file we translate ring theoretic properties of a property of ring homomorphisms P in properties of the category P.Under ⊤ R.

Main results

• CommRingCat.Under.hasFiniteLimits: If P is stable under finite products and equalizers, P.Under ⊤ R has finite limits.
• RingHom.HasStableEqualizers.preservesFiniteLimits_pushout: If P has stable equalizers, base change along arbitrary morphisms preserve finite limits.

theorem RingHom.HasFiniteProducts.isClosedUnderLimitsOfShape {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQp : HasFiniteProducts fun {R S : Type u} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => Q).underObj.IsClosedUnderFiniteProducts

theorem RingHom.HasEqualizers.isClosedUnderLimitsOfShape {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQe : HasEqualizers fun {R S : Type u} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => Q).underObj.IsClosedUnderLimitsOfShape CategoryTheory.Limits.WalkingParallelPair

@[implicit_reducible]

noncomputable def RingHom.HasFiniteProducts.createsFiniteProductsForget {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQp : HasFiniteProducts fun {R S : Type u} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.Limits.CreatesFiniteProducts (CategoryTheory.MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => Q) ⊤ R)

If Q is stable under finite products, the inclusion from the subcategory of Under R defined by Q creates finite products.

Equations

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

theorem RingHom.HasFiniteProducts.hasFiniteProducts {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQp : HasFiniteProducts fun {R S : Type u} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.Limits.HasFiniteProducts ((toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => Q).Under ⊤ R)

theorem RingHom.HasFiniteProducts.preservesFiniteProducts_pushout {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQp : HasFiniteProducts fun {R S : Type u} [CommRing R] [CommRing S] => Q) [(toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => Q).IsStableUnderCobaseChange] {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => Q) ⊤ f)

@[implicit_reducible]

noncomputable def RingHom.HasEqualizers.createsLimitsWalkingParallelPair {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQe : HasEqualizers fun {R S : Type u} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => Q) ⊤ R)

If Q is stable under equalizers, the inclusion from the subcategory of Under R defined by Q creates equalizers.

Equations

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

theorem RingHom.HasEqualizers.hasEqualizers {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQe : HasEqualizers fun {R S : Type u} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.Limits.HasEqualizers ((toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => Q).Under ⊤ R)

@[implicit_reducible]

noncomputable def CommRingCat.Under.createsFiniteLimitsForget {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQp : RingHom.HasFiniteProducts fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQe : RingHom.HasEqualizers fun {R S : Type u} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.Limits.CreatesFiniteLimits (CategoryTheory.MorphismProperty.Under.forget (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => Q) ⊤ R)

If Q is stable under finite products and equalizers, the inclusion from the subcategory of Under R defined by Q creates finite limits.

Equations

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

theorem CommRingCat.Under.hasFiniteLimits {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQp : RingHom.HasFiniteProducts fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQe : RingHom.HasEqualizers fun {R S : Type u} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.Limits.HasFiniteLimits ((RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => Q).Under ⊤ R)

theorem CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective {R S : CommRingCat} [Algebra ↑R ↑S] {A B : CategoryTheory.Under R} {f g : A ⟶ B} : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) (R.tensorProd S) ↔ Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))

theorem RingHom.HasStableEqualizers.preservesLimit_parallelPair_tensorProd {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPse : HasStableEqualizers fun {R S : Type u} [CommRing R] [CommRing S] => P) {R S : CommRingCat} [Algebra ↑R ↑S] {A B : CategoryTheory.Under R} (f g : A ⟶ B) (hA : P (CommRingCat.Hom.hom A.hom)) (hB : P (CommRingCat.Hom.hom B.hom)) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) (R.tensorProd S)

theorem RingHom.HasStableEqualizers.preservesEqualizers_pushout {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPi : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPe : HasEqualizers fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPse : HasStableEqualizers fun {R S : Type u} [CommRing R] [CommRing S] => P) [(toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => P).IsStableUnderCobaseChange] {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => P) ⊤ f)

theorem RingHom.HasStableEqualizers.preservesFiniteLimits_pushout {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPi : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPp : HasFiniteProducts fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPe : HasEqualizers fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPse : HasStableEqualizers fun {R S : Type u} [CommRing R] [CommRing S] => P) [(toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => P).IsStableUnderCobaseChange] {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => P) ⊤ f)

If P is a property of ring homs that is stable under finite products and equalizers, and the latter are preserved by arbitrary base change, pushout along any ring homomorphism preserves finite limits.