Documentation

Mathlib.RingTheory.RingHom.QuasiFinite

The meta properties of quasi-finite ring homomorphisms. #

source
def RingHom.QuasiFinite {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] (f : R →+* S) :
Prop

A ring hom R →+* S is quasi-finite if S is a quasi-finite R-algebra.

Equations
Instances For
    source
    theorem RingHom.QuasiFinite.toAlgebra {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.QuasiFinite) :
    Algebra.QuasiFinite R S

    Helper lemma for the algebraize tactic

    source
    theorem RingHom.quasiFinite_algebraMap {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] [Algebra R S] :
    (algebraMap R S).QuasiFinite ↔ Algebra.QuasiFinite R S
    source
    theorem RingHom.QuasiFinite.comp {T : Type u_3} [CommRing T] {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] {f : S →+* T} {g : R →+* S} (hf : f.QuasiFinite) (hg : g.QuasiFinite) :
    (f.comp g).QuasiFinite
    source
    theorem RingHom.QuasiFinite.of_comp {T : Type u_3} [CommRing T] {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] {f : S →+* T} {g : R →+* S} (h : (f.comp g).QuasiFinite) :
    f.QuasiFinite
    source
    theorem RingHom.QuasiFinite.comp_iff {T : Type u_3} [CommRing T] {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] {f : S →+* T} {g : R →+* S} (hg : g.QuasiFinite) :
    (f.comp g).QuasiFinite ↔ f.QuasiFinite
    source
    theorem RingHom.QuasiFinite.of_finite {T : Type u_3} [CommRing T] {S : Type u_5} [CommRing S] {f : S →+* T} (hf : f.Finite) :
    f.QuasiFinite
    source
    theorem RingHom.QuasiFinite.stableUnderComposition :
    StableUnderComposition fun {R S : Type u_6} [CommRing R] [CommRing S] => QuasiFinite
    source
    theorem RingHom.QuasiFinite.respectsIso :
    RespectsIso fun {R S : Type u_6} [CommRing R] [CommRing S] => QuasiFinite
    source
    theorem RingHom.QuasiFinite.isStableUnderBaseChange :
    IsStableUnderBaseChange fun {R S : Type u_6} [CommRing R] [CommRing S] => QuasiFinite
    source
    theorem RingHom.QuasiFinite.holdsForLocalizationAway :
    HoldsForLocalizationAway fun {R S : Type u_6} [CommRing R] [CommRing S] => QuasiFinite
    source
    theorem RingHom.QuasiFinite.ofLocalizationSpanTarget :
    OfLocalizationSpanTarget fun {R S : Type u_6} [CommRing R] [CommRing S] => QuasiFinite
    source
    theorem RingHom.QuasiFinite.propertyIsLocal :
    PropertyIsLocal fun {R S : Type u_6} [CommRing R] [CommRing S] => QuasiFinite
    source
    theorem RingHom.QuasiFinite.of_isIntegral_of_finiteType {R : Type u_6} {S : Type u_7} {T : Type u_8} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} (hf : f.IsIntegral) {g : S →+* T} (hg : g.IsStandardOpenImmersion) :
    (g.comp f).FiniteType → (g.comp f).QuasiFinite

    If T is both a finite type R-algebra, and the localization of an integral R-algebra, then T is quasi-finite over R

    source
    @[reducible, inline]
    abbrev RingHom.QuasiFiniteAt {R : Type u_6} {S : Type u_7} [CommRing R] [CommRing S] (f : R →+* S) (p : Ideal S) [p.IsPrime] :
    Prop

    The predicate for a ring hom being quasi-finite at a prime.

    Equations
    Instances For