Loogle!

Result

Found 63 declarations mentioning Algebra.Extension.Hom.

• Algebra.Extension.Hom.id 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) : P.Hom P
• Algebra.Extension.toInfinitesimal 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) : P.Hom P.infinitesimal
• Algebra.Extension.instFunLikeHomRing 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {P' : Algebra.Extension R S} : FunLike (P.Hom P') P.Ring P'.Ring
• Algebra.Extension.Hom 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Algebra.Extension R' S') [Algebra R R'] [Algebra S S'] : Type (max u_3 w)
• Algebra.Extension.Hom.toRingHom 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] (self : P.Hom P') : P.Ring →+* P'.Ring
• Algebra.Extension.Hom.id_comp 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') : (Algebra.Extension.Hom.id P').comp f = f
• Algebra.Extension.toBaseChange 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} (T : Type u_1) [CommRing T] [Algebra R T] : P.Hom P.baseChange
• Algebra.Extension.Cotangent.map 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') : P.Cotangent →ₗ[S] P'.Cotangent
• Algebra.Extension.Hom.ext 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} {inst✝ : CommRing R} {inst✝¹ : CommRing S} {inst✝² : Algebra R S} {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} {inst✝³ : CommRing R'} {inst✝⁴ : CommRing S'} {inst✝⁵ : Algebra R' S'} {P' : Algebra.Extension R' S'} {inst✝⁶ : Algebra R R'} {inst✝⁷ : Algebra S S'} {x y : P.Hom P'} (toRingHom : x.toRingHom = y.toRingHom) : x = y
• Algebra.Extension.Hom.ext_iff 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} {inst✝ : CommRing R} {inst✝¹ : CommRing S} {inst✝² : Algebra R S} {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} {inst✝³ : CommRing R'} {inst✝⁴ : CommRing S'} {inst✝⁵ : Algebra R' S'} {P' : Algebra.Extension R' S'} {inst✝⁶ : Algebra R R'} {inst✝⁷ : Algebra S S'} {x y : P.Hom P'} : x = y ↔ x.toRingHom = y.toRingHom
• Algebra.Extension.Hom.comp_id 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') : f.comp (Algebra.Extension.Hom.id P) = f
• Algebra.Extension.Hom.comp 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} {R'' : Type u_4} {S'' : Type u_5} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [Algebra R R'] [Algebra R' R''] [Algebra R R''] [Algebra S S'] [Algebra S' S''] [Algebra S S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] (f : P'.Hom P'') (g : P.Hom P') : P.Hom P''
• Algebra.Extension.Hom.toAlgHom 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') : P.Ring →ₐ[R] P'.Ring
• Algebra.Extension.Hom.comp_toRingHom 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} {R'' : Type u_4} {S'' : Type u_5} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [Algebra R R'] [Algebra R' R''] [Algebra R R''] [Algebra S S'] [Algebra S' S''] [Algebra S S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] (f : P'.Hom P'') (g : P.Hom P') : (f.comp g).toRingHom = f.toRingHom.comp g.toRingHom
• Algebra.Extension.Hom.algebraMap_toRingHom 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] (self : P.Hom P') (x : P.Ring) : (algebraMap P'.Ring S') (self.toRingHom x) = (algebraMap S S') ((algebraMap P.Ring S) x)
• Algebra.Extension.Hom.toAlgHom_apply 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_2} {S' : Type u_1} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (x : P.Ring) : f.toAlgHom x = f.toRingHom x
• Algebra.Extension.Hom.toRingHom_algebraMap 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] (self : P.Hom P') (x : R) : self.toRingHom ((algebraMap R P.Ring) x) = (algebraMap R' P'.Ring) ((algebraMap R R') x)
• Algebra.Extension.Hom.ofAlgHom 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Ring →ₐ[R] P'.Ring) (H : (IsScalarTower.toAlgHom R P'.Ring S').comp f = (IsScalarTower.toAlgHom R S S').comp (IsScalarTower.toAlgHom R P.Ring S)) : P.Hom P'
• Algebra.Extension.Cotangent.map_surjective_of_comap_eq 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {P' : Algebra.Extension R S} {f : P.Hom P'} (h : Function.Surjective ⇑f) (eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker) : Function.Surjective ⇑(Algebra.Extension.Cotangent.map f)
• Algebra.Extension.Cotangent.map_comp 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} {R'' : Type u_4} {S'' : Type u_5} [CommRing R''] [CommRing S''] [Algebra R'' S''] (P'' : Algebra.Extension R'' S'') [Algebra R R'] [Algebra R' R''] [Algebra R' S''] [Algebra S S'] [Algebra S' S''] [Algebra S S''] [Algebra R S'] [IsScalarTower R R' S'] [Algebra R R''] [IsScalarTower R R' R''] [IsScalarTower R' R'' S''] [Algebra R S''] [IsScalarTower R R'' S''] [IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') : Algebra.Extension.Cotangent.map (g.comp f) = ↑S (Algebra.Extension.Cotangent.map g) ∘ₗ Algebra.Extension.Cotangent.map f
• Algebra.Extension.Hom.mk 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] (toRingHom : P.Ring →+* P'.Ring) (toRingHom_algebraMap : ∀ (x : R), toRingHom ((algebraMap R P.Ring) x) = (algebraMap R' P'.Ring) ((algebraMap R R') x)) (algebraMap_toRingHom : ∀ (x : P.Ring), (algebraMap P'.Ring S') (toRingHom x) = (algebraMap S S') ((algebraMap P.Ring S) x)) : P.Hom P'
• Algebra.Extension.Hom.mapKer 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') [alg : Algebra P.Ring P'.Ring] (halg : algebraMap P.Ring P'.Ring = f.toRingHom) : ↥P.ker →ₗ[P.Ring] ↥P'.ker
• Algebra.Extension.Cotangent.map_ker_of_surjective 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {P' : Algebra.Extension R S} {f : P.Hom P'} (h : Function.Surjective ⇑f) (eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker) : Submodule.restrictScalars P.Ring (Algebra.Extension.Cotangent.map f).ker = Submodule.map Algebra.Extension.Cotangent.mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
• Algebra.Extension.Hom.mapKer_apply_coe 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] (f : P.Hom P') [alg : Algebra P.Ring P'.Ring] (halg : algebraMap P.Ring P'.Ring = f.toRingHom) (x : ↥P.ker) : ↑((f.mapKer halg) x) = f.toRingHom ↑x
• Algebra.Extension.Cotangent.map_mk 📋 Mathlib.RingTheory.Extension.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u_1} {S' : Type u_2} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (x : ↥P.ker) : (Algebra.Extension.Cotangent.map f) (Algebra.Extension.Cotangent.mk x) = Algebra.Extension.Cotangent.mk ⟨f.toAlgHom ↑x, ⋯⟩
• Algebra.Extension.defaultHom 📋 Mathlib.RingTheory.Extension.Generators
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) : (Algebra.Generators.self R S).toExtension.Hom P
• Algebra.Generators.Hom.toExtensionHom_id 📋 Mathlib.RingTheory.Extension.Generators
  {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S ι) : (Algebra.Generators.Hom.id P).toExtensionHom = Algebra.Extension.Hom.id P.toExtension
• Algebra.Generators.Hom.toExtensionHom 📋 Mathlib.RingTheory.Extension.Generators
  {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P') : P.toExtension.Hom P'.toExtension
• Algebra.Generators.baseChangeFromBaseChange 📋 Mathlib.RingTheory.Extension.Generators
  {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S ι) (T : Type u_2) [CommRing T] [Algebra R T] : P.toExtension.baseChange.Hom (Algebra.Generators.baseChange T P).toExtension
• Algebra.Generators.baseChangeToBaseChange 📋 Mathlib.RingTheory.Extension.Generators
  {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S ι) (T : Type u_2) [CommRing T] [Algebra R T] : (Algebra.Generators.baseChange T P).toExtension.Hom P.toExtension.baseChange
• Algebra.Generators.Hom.toExtensionHom_comp 📋 Mathlib.RingTheory.Extension.Generators
  {R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S ι) {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [CommRing R'] [CommRing S'] [Algebra R' S'] (P' : Algebra.Generators R' S' ι') {R'' : Type u_4} {S'' : Type u_5} {ι'' : Type u_6} [CommRing R''] [CommRing S''] [Algebra R'' S''] (P'' : Algebra.Generators R'' S'' ι'') [Algebra R R'] [Algebra R' R''] [Algebra R' S''] [Algebra S S'] [Algebra S' S''] [Algebra S S''] [Algebra R S'] [IsScalarTower R S S'] [Algebra R R''] [Algebra R S''] [IsScalarTower R R'' S''] [IsScalarTower R S S''] [IsScalarTower R' R'' S''] [IsScalarTower R' S' S''] [IsScalarTower S S' S''] [IsScalarTower R R' R''] [IsScalarTower R R' S'] (f : P'.Hom P'') (g : P.Hom P') : (f.comp g).toExtensionHom = f.toExtensionHom.comp g.toExtensionHom
• Algebra.Extension.H1Cotangent.equiv 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P₁ : Algebra.Extension R S} {P₂ : Algebra.Extension R S} (f₁ : P₁.Hom P₂) (f₂ : P₂.Hom P₁) : P₁.H1Cotangent ≃ₗ[S] P₂.H1Cotangent
• Algebra.Extension.H1Cotangent.map 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') : P.H1Cotangent →ₗ[S] P'.H1Cotangent
• Algebra.Extension.H1Cotangent.map_eq 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') : Algebra.Extension.H1Cotangent.map f = Algebra.Extension.H1Cotangent.map g
• Algebra.Extension.Hom.sub 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') : P.CotangentSpace →ₗ[S] P'.Cotangent
• Algebra.Extension.Hom.subToKer 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f g : P.Hom P') : P.Ring →ₗ[R] ↥P'.ker
• Algebra.Extension.Cotangent.map_sub_map 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') : Algebra.Extension.Cotangent.map f - Algebra.Extension.Cotangent.map g = f.sub g ∘ₗ P.cotangentComplex
• Algebra.Extension.CotangentSpace.map 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') : P.CotangentSpace →ₗ[S] P'.CotangentSpace
• Algebra.Extension.H1Cotangent.map_comp_apply 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [Algebra R R''] [Algebra S S''] [Algebra R S''] [IsScalarTower R R'' S''] [Algebra R' R''] [Algebra S' S''] [Algebra R' S''] [IsScalarTower R' R'' S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') (x : P.H1Cotangent) : (Algebra.Extension.H1Cotangent.map (g.comp f)) x = (Algebra.Extension.H1Cotangent.map g) ((Algebra.Extension.H1Cotangent.map f) x)
• Algebra.Extension.Cotangent.map_comp_h1Cotangentι 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') : Algebra.Extension.Cotangent.map f ∘ₗ Algebra.Extension.h1Cotangentι = ↑S Algebra.Extension.h1Cotangentι ∘ₗ Algebra.Extension.H1Cotangent.map f
• Algebra.Extension.H1Cotangent.map_comp 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [Algebra R R''] [Algebra S S''] [Algebra R S''] [IsScalarTower R R'' S''] [Algebra R' R''] [Algebra S' S''] [Algebra R' S''] [IsScalarTower R' R'' S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') : Algebra.Extension.H1Cotangent.map (g.comp f) = ↑S (Algebra.Extension.H1Cotangent.map g) ∘ₗ Algebra.Extension.H1Cotangent.map f
• Algebra.Extension.Hom.subToKer_apply_coe 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f g : P.Hom P') (c : P.Ring) : ↑((f.subToKer g) c) = f.toRingHom c - g.toRingHom c
• Algebra.Extension.H1Cotangent.map_apply_coe 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (c : ↥P.cotangentComplex.ker) : ↑((Algebra.Extension.H1Cotangent.map f) c) = (Algebra.Extension.Cotangent.map f) ↑c
• Algebra.Extension.Hom.sub_aux 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f g : P.Hom P') (x y : P.Ring) : f.toAlgHom (x * y) - g.toAlgHom (x * y) - (P'.σ ((algebraMap P.Ring S') x) * (f.toAlgHom y - g.toAlgHom y) + P'.σ ((algebraMap P.Ring S') y) * (f.toAlgHom x - g.toAlgHom x)) ∈ P'.ker ^ 2
• Algebra.Extension.H1Cotangent.equiv_apply 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P₁ : Algebra.Extension R S} {P₂ : Algebra.Extension R S} (f₁ : P₁.Hom P₂) (f₂ : P₂.Hom P₁) (c : ↥P₁.cotangentComplex.ker) : (Algebra.Extension.H1Cotangent.equiv f₁ f₂) c = ⟨(Algebra.Extension.Cotangent.map f₁) ↑c, ⋯⟩
• Algebra.Extension.CotangentSpace.map_cotangentComplex 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (x : P.Cotangent) : (Algebra.Extension.CotangentSpace.map f) (P.cotangentComplex x) = P'.cotangentComplex ((Algebra.Extension.Cotangent.map f) x)
• Algebra.Extension.Hom.sub_one_tmul 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') (x : P.Ring) : (f.sub g) (1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x) = Algebra.Extension.Cotangent.mk ((f.subToKer g) x)
• Algebra.Extension.CotangentSpace.map_tmul 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (x : S) (y : P.Ring) : (Algebra.Extension.CotangentSpace.map f) (x ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) y) = (algebraMap S S') x ⊗ₜ[P'.Ring] (KaehlerDifferential.D R' P'.Ring) (f.toAlgHom y)
• Algebra.Extension.Hom.sub_tmul 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') (r : S) (x : P.Ring) : (f.sub g) (r ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x) = r • Algebra.Extension.Cotangent.mk ((f.subToKer g) x)
• Algebra.Extension.CotangentSpace.map_comp_cotangentComplex 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') : Algebra.Extension.CotangentSpace.map f ∘ₗ P.cotangentComplex = ↑S P'.cotangentComplex ∘ₗ Algebra.Extension.Cotangent.map f
• Algebra.Extension.CotangentSpace.map_tmul_eq_tmul_map 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (x : S) (y : Ω[P.Ring⁄R]) : (Algebra.Extension.CotangentSpace.map f) (x ⊗ₜ[P.Ring] y) = (algebraMap S S') x ⊗ₜ[P'.Ring] (KaehlerDifferential.map R R' P.Ring P'.Ring) y
• Algebra.Extension.CotangentSpace.map_comp_apply 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [Algebra R R''] [Algebra S S''] [Algebra R S''] [IsScalarTower R R'' S''] [Algebra R' R''] [Algebra S' S''] [Algebra R' S''] [IsScalarTower R' R'' S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') (x : P.CotangentSpace) : (Algebra.Extension.CotangentSpace.map (g.comp f)) x = (Algebra.Extension.CotangentSpace.map g) ((Algebra.Extension.CotangentSpace.map f) x)
• Algebra.Extension.CotangentSpace.map_comp 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [Algebra R R''] [Algebra S S''] [Algebra R S''] [IsScalarTower R R'' S''] [Algebra R' R''] [Algebra S' S''] [Algebra R' S''] [IsScalarTower R' R'' S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') : Algebra.Extension.CotangentSpace.map (g.comp f) = ↑S (Algebra.Extension.CotangentSpace.map g) ∘ₗ Algebra.Extension.CotangentSpace.map f
• Algebra.Extension.CotangentSpace.map_sub_map 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') : Algebra.Extension.CotangentSpace.map f - Algebra.Extension.CotangentSpace.map g = ↑S P'.cotangentComplex ∘ₗ f.sub g
• Algebra.Extension.homInfinitesimal 📋 Mathlib.RingTheory.Smooth.Basic
  {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (P₁ : Algebra.Extension R A) (P₂ : Algebra.Extension R A) [Algebra.FormallySmooth R P₁.Ring] : P₁.infinitesimal.Hom P₂.infinitesimal
• Algebra.Extension.H1Cotangent.equivOfFormallySmooth_toLinearMap 📋 Mathlib.RingTheory.Smooth.Basic
  {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {P₁ : Algebra.Extension R A} {P₂ : Algebra.Extension R A} (f : P₁.Hom P₂) [Algebra.FormallySmooth R P₁.Ring] [Algebra.FormallySmooth R P₂.Ring] : ↑(Algebra.Extension.H1Cotangent.equivOfFormallySmooth P₁ P₂) = Algebra.Extension.H1Cotangent.map f
• Algebra.Extension.H1Cotangent.equivOfFormallySmooth_apply 📋 Mathlib.RingTheory.Smooth.Basic
  {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {P₁ : Algebra.Extension R A} {P₂ : Algebra.Extension R A} (f : P₁.Hom P₂) [Algebra.FormallySmooth R P₁.Ring] [Algebra.FormallySmooth R P₂.Ring] (x : P₁.H1Cotangent) : (Algebra.Extension.H1Cotangent.equivOfFormallySmooth P₁ P₂) x = (Algebra.Extension.H1Cotangent.map f) x
• Algebra.Extension.tensorCotangentSpaceOfFormallyEtale 📋 Mathlib.RingTheory.Etale.Kaehler
  {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {P : Algebra.Extension R S} {Q : Algebra.Extension R T} (f : P.Hom Q) (H : f.toRingHom.FormallyEtale) : TensorProduct S T P.CotangentSpace ≃ₗ[T] Q.CotangentSpace
• Algebra.Extension.tensorCotangentInvFun 📋 Mathlib.RingTheory.Etale.Kaehler
  {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] {P : Algebra.Extension R S} {Q : Algebra.Extension R T} (f : P.Hom Q) [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom) (H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))) : Q.Cotangent →+ TensorProduct S T P.Cotangent
• Algebra.Extension.tensorCotangent 📋 Mathlib.RingTheory.Etale.Kaehler
  {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] {P : Algebra.Extension R S} {Q : Algebra.Extension R T} (f : P.Hom Q) [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom) (H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))) : TensorProduct S T P.Cotangent ≃ₗ[T] Q.Cotangent
• Algebra.Extension.tensorH1CotangentOfFormallyEtale 📋 Mathlib.RingTheory.Etale.Kaehler
  {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {P : Algebra.Extension R S} {Q : Algebra.Extension R T} (f : P.Hom Q) [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom) [Module.Flat S T] (H₁ : f.toRingHom.FormallyEtale) (H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))) : TensorProduct S T P.H1Cotangent ≃ₗ[T] Q.H1Cotangent
• Algebra.Extension.tensorCotangentInvFun_smul_mk 📋 Mathlib.RingTheory.Etale.Kaehler
  {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] {P : Algebra.Extension R S} {Q : Algebra.Extension R T} (f : P.Hom Q) [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom) (H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))) (x : Q.Ring) (y : ↥P.ker) : (Algebra.Extension.tensorCotangentInvFun f halg H) (x • Algebra.Extension.Cotangent.mk ⟨f.toRingHom ↑y, ⋯⟩) = x • 1 ⊗ₜ[S] Algebra.Extension.Cotangent.mk y
• Algebra.Extension.toExtendScalars 📋 Mathlib.RingTheory.Extension.ExtendScalars
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) : P.Hom P.extendScalars

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c