Documentation

Mathlib.Algebra.Category.Ring.Under.Property

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 #

source
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
source
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
source
@[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.
Instances For
    source
    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)
    source
    @[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.
    Instances For
      source
      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)
      source
      @[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.
      Instances For
        source
        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)