Documentation

Mathlib.RingTheory.RingHom.EssFiniteType

Meta properties of essentially of finite type ring homomorphisms #

source
theorem RingHom.EssFiniteType.comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} {g : S →+* T} (hf : f.EssFiniteType) (hg : g.EssFiniteType) :
(g.comp f).EssFiniteType
source
theorem RingHom.EssFiniteType.comp_iff {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} {g : S →+* T} (hf : f.EssFiniteType) :
(g.comp f).EssFiniteType ↔ g.EssFiniteType
source
theorem RingHom.EssFiniteType.of_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) {g : S →+* T} (h : (g.comp f).EssFiniteType) :
g.EssFiniteType
source
theorem RingHom.EssFiniteType.stableUnderComposition :
StableUnderComposition fun {R S : Type u_4} [CommRing R] [CommRing S] => EssFiniteType
source
theorem RingHom.EssFiniteType.respectsIso :
RespectsIso fun {R S : Type u_4} [CommRing R] [CommRing S] => EssFiniteType
source
theorem RingHom.EssFiniteType.isStableUnderBaseChange :
IsStableUnderBaseChange fun {R S : Type u_4} [CommRing R] [CommRing S] => EssFiniteType
source
theorem RingHom.EssFiniteType.holdsForLocalization :
HoldsForLocalization fun {R S : Type u_4} [CommRing R] [CommRing S] => EssFiniteType
source
theorem RingHom.EssFiniteType.residueFieldMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} [IsLocalRing R] [IsLocalRing S] [IsLocalHom f] (hf : f.EssFiniteType) :
(IsLocalRing.ResidueField.map f).EssFiniteType