Documentation

Mathlib.RingTheory.RingHomProperties

Properties of ring homomorphisms #

We provide the basic framework for talking about properties of ring homomorphisms. The following meta-properties of predicates on ring homomorphisms are defined

def RingHom.RespectsIso (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) :

A property RespectsIso if it still holds when composed with an isomorphism

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem RingHom.RespectsIso.cancel_left_isIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (hP : RingHom.RespectsIso P) {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R S) (g : S T) [CategoryTheory.IsIso f] :
    theorem RingHom.RespectsIso.cancel_right_isIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (hP : RingHom.RespectsIso P) {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R S) (g : S T) [CategoryTheory.IsIso g] :
    theorem RingHom.RespectsIso.is_localization_away_iff {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (hP : RingHom.RespectsIso P) {R : Type u} {S : Type u} (R' : Type u) (S' : Type u) [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] (f : R →+* S) (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] :
    def RingHom.StableUnderComposition (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) :

    A property is StableUnderComposition if the composition of two such morphisms still falls in the class.

    Equations
    Instances For
      theorem RingHom.StableUnderComposition.respectsIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (hP : RingHom.StableUnderComposition P) (hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P e.toRingHom) :
      def RingHom.StableUnderBaseChange (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) :

      A morphism property P is StableUnderBaseChange if P(S →+* A) implies P(B →+* A ⊗[S] B).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem RingHom.StableUnderBaseChange.mk (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) (h₁ : RingHom.RespectsIso P) (h₂ : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], P (algebraMap R T)P Algebra.TensorProduct.includeLeftRingHom) :
        theorem RingHom.StableUnderBaseChange.pushout_inl (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) (hP : RingHom.StableUnderBaseChange P) (hP' : RingHom.RespectsIso P) {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R S) (g : R T) (H : P g) :
        def RingHom.toMorphismProperty (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) :

        The categorical MorphismProperty associated to a property of ring homs expressed non-categorical terms.

        Equations
        Instances For
          theorem RingHom.toMorphismProperty_respectsIso_iff {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} :
          (RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => P).RespectsIso