Loogle!
Result
Found 1384 definitions whose name contains "differ". Of these, only the first 200 are shown.
- Ideal.Filtration.Stable.bounded_difference π Mathlib.RingTheory.Filtration
{R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F F' : I.Filtration M} (h : F.Stable) (h' : F'.Stable) (e : F.N 0 = F'.N 0) : β nβ, β (n : β), F.N (n + nβ) β€ F'.N n β§ F'.N (n + nβ) β€ F.N n - KaehlerDifferential π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Type v - instAddCommGroupKaehlerDifferential π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : AddCommGroup (Ξ©[SβR]) - instNonemptyKaehlerDifferential π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Nonempty (Ξ©[SβR]) - KaehlerDifferential.subsingleton_of_surjective π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (h : Function.Surjective β(algebraMap R S)) : Subsingleton (Ξ©[SβR]) - KaehlerDifferential.kerTotal π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Submodule S (S ββ S) - KaehlerDifferential.module' π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {R' : Type u_2} [CommRing R'] [Algebra R' S] [SMulCommClass R R' S] : Module R' (Ξ©[SβR]) - KaehlerDifferential.ideal π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Ideal (TensorProduct R S S) - KaehlerDifferential.finite π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] : Module.Finite S (Ξ©[SβR]) - KaehlerDifferential.ideal_fg π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] : (KaehlerDifferential.ideal R S).FG - KaehlerDifferential.module π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Module (TensorProduct R S S) (Ξ©[SβR]) - KaehlerDifferential.DLinearMap π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : S ββ[R] Ξ©[SβR] - KaehlerDifferential.D π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Derivation R S (Ξ©[SβR]) - KaehlerDifferential.map π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] : Ξ©[AβR] ββ[A] Ξ©[BβS] - Derivation.liftKaehlerDifferential π Mathlib.RingTheory.Kaehler.Basic
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) : Ξ©[SβR] ββ[S] M - KaehlerDifferential.map_surjective π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (B : Type u_3) [CommRing B] [Algebra S B] [Algebra R B] [IsScalarTower R S B] : Function.Surjective β(KaehlerDifferential.map R S B B) - KaehlerDifferential.map_surjective_of_surjective π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] (h : Function.Surjective β(algebraMap A B)) : Function.Surjective β(KaehlerDifferential.map R S A B) - Derivation.liftKaehlerDifferential_D π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (KaehlerDifferential.D R S).liftKaehlerDifferential = LinearMap.id - KaehlerDifferential.isScalarTower_of_tower π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {Rβ : Type u_2} {Rβ : Type u_3} [CommRing Rβ] [CommRing Rβ] [Algebra Rβ S] [Algebra Rβ S] [SMul Rβ Rβ] [SMulCommClass R Rβ S] [SMulCommClass R Rβ S] [IsScalarTower Rβ Rβ S] : IsScalarTower Rβ Rβ (Ξ©[SβR]) - KaehlerDifferential.quotKerTotalEquiv π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : ((S ββ S) β§Έ KaehlerDifferential.kerTotal R S) ββ[S] Ξ©[SβR] - KaehlerDifferential.mapBaseChange π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] : TensorProduct A B (Ξ©[AβR]) ββ[B] Ξ©[BβR] - KaehlerDifferential.span_range_derivation π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Submodule.span S (Set.range β(KaehlerDifferential.D R S)) = β€ - KaehlerDifferential.kerCotangentToTensor π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] : (RingHom.ker (algebraMap A B)).Cotangent ββ[A] TensorProduct A B (Ξ©[AβR]) - KaehlerDifferential.kerToTensor π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] : β₯(RingHom.ker (algebraMap A B)) ββ[A] TensorProduct A B (Ξ©[AβR]) - KaehlerDifferential.linearMapEquivDerivation π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] : (Ξ©[SβR] ββ[S] M) ββ[S] Derivation R S M - KaehlerDifferential.derivationQuotKerTotal π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Derivation R S ((S ββ S) β§Έ KaehlerDifferential.kerTotal R S) - KaehlerDifferential.linearCombination_surjective π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Function.Surjective β(Finsupp.linearCombination S β(KaehlerDifferential.D R S)) - KaehlerDifferential.total_surjective π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Function.Surjective β(Finsupp.linearCombination S β(KaehlerDifferential.D R S)) - Derivation.liftKaehlerDifferential_comp_D π Mathlib.RingTheory.Kaehler.Basic
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D' : Derivation R S M) (x : S) : D'.liftKaehlerDifferential ((KaehlerDifferential.D R S) x) = D' x - KaehlerDifferential.span_range_eq_ideal π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Ideal.span (Set.range fun s => 1 ββ[R] s - s ββ[R] 1) = KaehlerDifferential.ideal R S - KaehlerDifferential.kerTotal.eq_1 π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : KaehlerDifferential.kerTotal R S = Submodule.span S (((Set.range fun x => ((funβ | x.1 => 1) + funβ | x.2 => 1) - funβ | x.1 + x.2 => 1) βͺ Set.range fun x => ((funβ | x.2 => x.1) + funβ | x.1 => x.2) - funβ | x.1 * x.2 => 1) βͺ Set.range fun x => funβ | (algebraMap R S) x => 1) - KaehlerDifferential.kerTotal_eq π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : LinearMap.ker (Finsupp.linearCombination S β(KaehlerDifferential.D R S)) = KaehlerDifferential.kerTotal R S - KaehlerDifferential.isScalarTower' π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : IsScalarTower R (TensorProduct R S S) (Ξ©[SβR]) - KaehlerDifferential.map_D π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] (x : A) : (KaehlerDifferential.map R S A B) ((KaehlerDifferential.D R A) x) = (KaehlerDifferential.D S B) ((algebraMap A B) x) - instIsScalarTowerTensorProductKaehlerDifferential π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : IsScalarTower S (TensorProduct R S S) (Ξ©[SβR]) - KaehlerDifferential.tensorProductTo_surjective π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Function.Surjective β(KaehlerDifferential.D R S).tensorProductTo - KaehlerDifferential.one_smul_sub_smul_one_mem_ideal π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (a : S) : 1 ββ[R] a - a ββ[R] 1 β KaehlerDifferential.ideal R S - KaehlerDifferential.mapBaseChange_surjective π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective β(algebraMap A B)) : Function.Surjective β(KaehlerDifferential.mapBaseChange R A B) - KaehlerDifferential.exact_mapBaseChange_map π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] : Function.Exact β(KaehlerDifferential.mapBaseChange R A B) β(KaehlerDifferential.map R A B B) - KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x : S) : ((KaehlerDifferential.kerTotal R S).mkQ funβ | 1 => x) = 0 - KaehlerDifferential.kerTotal_mkQ_single_algebraMap π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x : R) (y : S) : ((KaehlerDifferential.kerTotal R S).mkQ funβ | (algebraMap R S) x => y) = 0 - KaehlerDifferential.kerTotal_map' π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective β(algebraMap A B)) : Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ββ Finsupp.lmapDomain A A β(algebraMap A B)) (KaehlerDifferential.kerTotal R A β Submodule.span A (Set.range fun x => funβ | (algebraMap R A) x => 1)) = Submodule.restrictScalars A (KaehlerDifferential.kerTotal R B) - KaehlerDifferential.fromIdeal π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : β₯(KaehlerDifferential.ideal R S) ββ[TensorProduct R S S] Ξ©[SβR] - KaehlerDifferential.mapBaseChange_tmul π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (x : B) (y : Ξ©[AβR]) : (KaehlerDifferential.mapBaseChange R A B) (x ββ[A] y) = x β’ (KaehlerDifferential.map R R A B) y - KaehlerDifferential.kerTotal_map π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] (h : Function.Surjective β(algebraMap A B)) : Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ββ Finsupp.lmapDomain A A β(algebraMap A B)) (KaehlerDifferential.kerTotal R A) β Submodule.span A (Set.range fun x => funβ | (algebraMap S B) x => 1) = Submodule.restrictScalars A (KaehlerDifferential.kerTotal S B) - KaehlerDifferential.submodule_span_range_eq_ideal π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Submodule.span S (Set.range fun s => 1 ββ[R] s - s ββ[R] 1) = Submodule.restrictScalars S (KaehlerDifferential.ideal R S) - KaehlerDifferential.kerToTensor_apply π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] (x : β₯(RingHom.ker (algebraMap A B))) : (KaehlerDifferential.kerToTensor R A B) x = 1 ββ[A] (KaehlerDifferential.D R A) βx - KaehlerDifferential.linearMapEquivDerivation_apply_apply π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (m : Ξ©[SβR] ββ[S] M) (aβ : S) : ((KaehlerDifferential.linearMapEquivDerivation R S) m) aβ = m ((KaehlerDifferential.D R S) aβ) - KaehlerDifferential.linearMapEquivDerivation_symm_apply π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) : (KaehlerDifferential.linearMapEquivDerivation R S).symm D = D.liftKaehlerDifferential - KaehlerDifferential.range_mapBaseChange π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] : LinearMap.range (KaehlerDifferential.mapBaseChange R A B) = LinearMap.ker (KaehlerDifferential.map R A B B) - KaehlerDifferential.ker_map_of_surjective π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective β(algebraMap A B)) : LinearMap.ker (KaehlerDifferential.map R R A B) = Submodule.map (Finsupp.linearCombination A β(KaehlerDifferential.D R A)) (LinearMap.ker (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ββ Finsupp.lmapDomain A A β(algebraMap A B))) - KaehlerDifferential.ker_map π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] : LinearMap.ker (KaehlerDifferential.map R S A B) = Submodule.map (Finsupp.linearCombination A β(KaehlerDifferential.D R A)) (Submodule.comap (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ββ Finsupp.lmapDomain A A β(algebraMap A B)) (Submodule.restrictScalars A (KaehlerDifferential.kerTotal S B))) - KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential ββ Finsupp.linearCombination S β(KaehlerDifferential.D R S) = (KaehlerDifferential.kerTotal R S).mkQ - KaehlerDifferential.derivationQuotKerTotal_lift_comp_total π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential ββ Finsupp.linearCombination S β(KaehlerDifferential.D R S) = (KaehlerDifferential.kerTotal R S).mkQ - Derivation.liftKaehlerDifferential_comp π Mathlib.RingTheory.Kaehler.Basic
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) : D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S) = D - KaehlerDifferential.derivationQuotKerTotal_apply π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x : S) : (KaehlerDifferential.derivationQuotKerTotal R S) x = (KaehlerDifferential.kerTotal R S).mkQ funβ | x => 1 - KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective β(algebraMap A B)) : Function.Exact β(KaehlerDifferential.kerCotangentToTensor R A B) β(KaehlerDifferential.mapBaseChange R A B) - KaehlerDifferential.kerTotal_mkQ_single_smul π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (r : R) (x y : S) : ((KaehlerDifferential.kerTotal R S).mkQ funβ | r β’ x => y) = r β’ (KaehlerDifferential.kerTotal R S).mkQ funβ | x => y - KaehlerDifferential.quotKerTotalEquiv_symm_apply π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (a : Ξ©[SβR]) : (KaehlerDifferential.quotKerTotalEquiv R S).symm a = (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential a - KaehlerDifferential.kerCotangentToTensor_toCotangent π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] (x : β₯(RingHom.ker (algebraMap A B))) : (KaehlerDifferential.kerCotangentToTensor R A B) ((RingHom.ker (algebraMap A B)).toCotangent x) = 1 ββ[A] (KaehlerDifferential.D R A) βx - KaehlerDifferential.map_compDer π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] : (KaehlerDifferential.map R S A B).compDer (KaehlerDifferential.D R A) = Derivation.compAlgebraMap A (Derivation.restrictScalars R (KaehlerDifferential.D S B)) - KaehlerDifferential.kerTotal_mkQ_single_add π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x y z : S) : ((KaehlerDifferential.kerTotal R S).mkQ funβ | x + y => z) = ((KaehlerDifferential.kerTotal R S).mkQ funβ | x => z) + (KaehlerDifferential.kerTotal R S).mkQ funβ | y => z - KaehlerDifferential.kerTotal_mkQ_single_mul π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x y z : S) : ((KaehlerDifferential.kerTotal R S).mkQ funβ | x * y => z) = ((KaehlerDifferential.kerTotal R S).mkQ funβ | y => z * x) + (KaehlerDifferential.kerTotal R S).mkQ funβ | x => z * y - KaehlerDifferential.range_kerCotangentToTensor π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective β(algebraMap A B)) : LinearMap.range (KaehlerDifferential.kerCotangentToTensor R A B) = Submodule.restrictScalars A (LinearMap.ker (KaehlerDifferential.mapBaseChange R A B)) - Derivation.liftKaehlerDifferential_unique π Mathlib.RingTheory.Kaehler.Basic
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (f f' : Ξ©[SβR] ββ[S] M) (hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)) : f = f' - Derivation.liftKaehlerDifferential_unique_iff π Mathlib.RingTheory.Kaehler.Basic
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] {f f' : Ξ©[SβR] ββ[S] M} : f = f' β f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S) - KaehlerDifferential.DLinearMap_apply π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (s : S) : (KaehlerDifferential.DLinearMap R S) s = (KaehlerDifferential.ideal R S).toCotangent β¨1 ββ[R] s - s ββ[R] 1, β―β© - KaehlerDifferential.D_apply π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (s : S) : (KaehlerDifferential.D R S) s = (KaehlerDifferential.ideal R S).toCotangent β¨1 ββ[R] s - s ββ[R] 1, β―β© - KaehlerDifferential.D_tensorProductTo π Mathlib.RingTheory.Kaehler.Basic
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (x : β₯(KaehlerDifferential.ideal R S)) : (KaehlerDifferential.D R S).tensorProductTo βx = (KaehlerDifferential.ideal R S).toCotangent x - Derivation.liftKaehlerDifferential_apply π Mathlib.RingTheory.Kaehler.Basic
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) (x : β₯(KaehlerDifferential.ideal R S)) : D.liftKaehlerDifferential ((KaehlerDifferential.ideal R S).toCotangent x) = D.tensorProductTo βx - KaehlerDifferential.quotKerTotalEquiv_symm_comp_D π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (β(KaehlerDifferential.quotKerTotalEquiv R S).symm).compDer (KaehlerDifferential.D R S) = KaehlerDifferential.derivationQuotKerTotal R S - KaehlerDifferential.quotKerTotalEquiv_apply π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (aβ : (S ββ S) β§Έ (KaehlerDifferential.kerTotal R S).toAddSubgroup) : (KaehlerDifferential.quotKerTotalEquiv R S) aβ = (QuotientAddGroup.lift (KaehlerDifferential.kerTotal R S).toAddSubgroup (Finsupp.linearCombination S β(KaehlerDifferential.D R S)).toAddMonoidHom β―) aβ - KaehlerDifferential.endEquiv π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Module.End S (Ξ©[SβR]) β { f // (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S } - KaehlerDifferential.quotientCotangentIdeal π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : ((TensorProduct R S S β§Έ KaehlerDifferential.ideal R S ^ 2) β§Έ (KaehlerDifferential.ideal R S).cotangentIdeal) ββ[S] S - KaehlerDifferential.quotientCotangentIdealRingEquiv π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (TensorProduct R S S β§Έ KaehlerDifferential.ideal R S ^ 2) β§Έ (KaehlerDifferential.ideal R S).cotangentIdeal β+* S - KaehlerDifferential.End_equiv_aux π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (f : S ββ[R] TensorProduct R S S β§Έ KaehlerDifferential.ideal R S ^ 2) : (Ideal.Quotient.mkβ R (KaehlerDifferential.ideal R S).cotangentIdeal).comp f = IsScalarTower.toAlgHom R S ((TensorProduct R S S β§Έ KaehlerDifferential.ideal R S ^ 2) β§Έ (KaehlerDifferential.ideal R S).cotangentIdeal) β (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S - KaehlerDifferential.endEquivAuxEquiv π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : { f // (Ideal.Quotient.mkβ R (KaehlerDifferential.ideal R S).cotangentIdeal).comp f = IsScalarTower.toAlgHom R S ((TensorProduct R S S β§Έ KaehlerDifferential.ideal R S ^ 2) β§Έ (KaehlerDifferential.ideal R S).cotangentIdeal) } β { f // (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S } - KaehlerDifferential.endEquivDerivation' π Mathlib.RingTheory.Kaehler.Basic
(R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Derivation R S (Ξ©[SβR]) ββ[R] Derivation R S β₯(KaehlerDifferential.ideal R S).cotangentIdeal - CommRingCat.KaehlerDifferential.D π Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
{A B : CommRingCat} (f : A βΆ B) : (CommRingCat.KaehlerDifferential f).Derivation f - CommRingCat.KaehlerDifferential π Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
{A B : CommRingCat} (f : A βΆ B) : ModuleCat βB - CommRingCat.KaehlerDifferential.d π Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
{A B : CommRingCat} {f : A βΆ B} (b : βB) : β(CommRingCat.KaehlerDifferential f) - CommRingCat.KaehlerDifferential.map π Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
{A B A' B' : CommRingCat} {f : A βΆ B} {f' : A' βΆ B'} {g : A βΆ A'} {g' : B βΆ B'} (fac : CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g') : CommRingCat.KaehlerDifferential f βΆ (ModuleCat.restrictScalars g').obj (CommRingCat.KaehlerDifferential f') - CommRingCat.KaehlerDifferential.ext π Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
{A B : CommRingCat} {f : A βΆ B} {M : ModuleCat βB} {Ξ± Ξ² : CommRingCat.KaehlerDifferential f βΆ M} (h : β (b : βB), Ξ±.hom (CommRingCat.KaehlerDifferential.d b) = Ξ².hom (CommRingCat.KaehlerDifferential.d b)) : Ξ± = Ξ² - CommRingCat.KaehlerDifferential.ext_iff π Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
{A B : CommRingCat} {f : A βΆ B} {M : ModuleCat βB} {Ξ± Ξ² : CommRingCat.KaehlerDifferential f βΆ M} : Ξ± = Ξ² β β (b : βB), Ξ±.hom (CommRingCat.KaehlerDifferential.d b) = Ξ².hom (CommRingCat.KaehlerDifferential.d b) - CommRingCat.KaehlerDifferential.map_d π Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
{A B A' B' : CommRingCat} {f : A βΆ B} {f' : A' βΆ B'} {g : A βΆ A'} {g' : B βΆ B'} (fac : CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g') (b : βB) : (CommRingCat.KaehlerDifferential.map fac).hom (CommRingCat.KaehlerDifferential.d b) = CommRingCat.KaehlerDifferential.d (g' b) - PresheafOfModules.DifferentialsConstruction.instHasDifferentials π Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
{D : Type uβ} [CategoryTheory.Category.{vβ, uβ} D] {S' R : CategoryTheory.Functor Dα΅α΅ CommRingCat} (Ο' : S' βΆ R) : PresheafOfModules.HasDifferentials Ο' - PresheafOfModules.DifferentialsConstruction.derivation' π Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
{D : Type uβ} [CategoryTheory.Category.{vβ, uβ} D] {S' R : CategoryTheory.Functor Dα΅α΅ CommRingCat} (Ο' : S' βΆ R) : (PresheafOfModules.DifferentialsConstruction.relativeDifferentials' Ο').Derivation' Ο' - PresheafOfModules.DifferentialsConstruction.isUniversal' π Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
{D : Type uβ} [CategoryTheory.Category.{vβ, uβ} D] {S' R : CategoryTheory.Functor Dα΅α΅ CommRingCat} (Ο' : S' βΆ R) : PresheafOfModules.Derivation.Universal (PresheafOfModules.DifferentialsConstruction.derivation' Ο') - PresheafOfModules.HasDifferentials π Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
{C : Type uβ} [CategoryTheory.Category.{vβ, uβ} C] {D : Type uβ} [CategoryTheory.Category.{vβ, uβ} D] {S : CategoryTheory.Functor Cα΅α΅ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dα΅α΅ CommRingCat} (Ο : S βΆ F.op.comp R) : Prop - PresheafOfModules.DifferentialsConstruction.relativeDifferentials' π Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
{D : Type uβ} [CategoryTheory.Category.{vβ, uβ} D] {S' R : CategoryTheory.Functor Dα΅α΅ CommRingCat} (Ο' : S' βΆ R) : PresheafOfModules (R.comp (CategoryTheory.forgetβ CommRingCat RingCat)) - PresheafOfModules.HasDifferentials.exists_universal_derivation π Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
{C : Type uβ} {instβ : CategoryTheory.Category.{vβ, uβ} C} {D : Type uβ} {instβΒΉ : CategoryTheory.Category.{vβ, uβ} D} {S : CategoryTheory.Functor Cα΅α΅ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dα΅α΅ CommRingCat} {Ο : S βΆ F.op.comp R} [self : PresheafOfModules.HasDifferentials Ο] : β M d, Nonempty d.Universal - PresheafOfModules.HasDifferentials.mk π Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
{C : Type uβ} [CategoryTheory.Category.{vβ, uβ} C] {D : Type uβ} [CategoryTheory.Category.{vβ, uβ} D] {S : CategoryTheory.Functor Cα΅α΅ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dα΅α΅ CommRingCat} {Ο : S βΆ F.op.comp R} (exists_universal_derivation : β M d, Nonempty d.Universal) : PresheafOfModules.HasDifferentials Ο - PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_obj π Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
{D : Type uβ} [CategoryTheory.Category.{vβ, uβ} D] {S' R : CategoryTheory.Functor Dα΅α΅ CommRingCat} (Ο' : S' βΆ R) (X : Dα΅α΅) : (PresheafOfModules.DifferentialsConstruction.relativeDifferentials' Ο').obj X = CommRingCat.KaehlerDifferential (Ο'.app X) - PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map π Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
{D : Type uβ} [CategoryTheory.Category.{vβ, uβ} D] {S' R : CategoryTheory.Functor Dα΅α΅ CommRingCat} (Ο' : S' βΆ R) {Xβ Yβ : Dα΅α΅} (f : Xβ βΆ Yβ) : (PresheafOfModules.DifferentialsConstruction.relativeDifferentials' Ο').map f = CommRingCat.KaehlerDifferential.map β― - PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d π Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
{D : Type uβ} [CategoryTheory.Category.{vβ, uβ} D] {S' R : CategoryTheory.Functor Dα΅α΅ CommRingCat} (Ο' : S' βΆ R) {X Y : Dα΅α΅} (f : X βΆ Y) (x : β(R.obj X)) : ((PresheafOfModules.DifferentialsConstruction.relativeDifferentials' Ο').map f).hom (CommRingCat.KaehlerDifferential.d x) = CommRingCat.KaehlerDifferential.d ((R.map f) x) - CategoryTheory.DifferentialObject π Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) [AddMonoidWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : Type (max u v) - CategoryTheory.DifferentialObject.categoryOfDifferentialObjects π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.Category.{v, max u v} (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.obj π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) : C - CategoryTheory.DifferentialObject.Hom π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X Y : CategoryTheory.DifferentialObject S C) : Type v - CategoryTheory.DifferentialObject.Hom.id π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : X.Hom X - CategoryTheory.DifferentialObject.forget π Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) [AddMonoidWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) C - CategoryTheory.DifferentialObject.concreteCategoryOfDifferentialObjects π Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.ConcreteCategory (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.forget_faithful π Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) [AddMonoidWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : (CategoryTheory.DifferentialObject.forget S C).Faithful - CategoryTheory.DifferentialObject.instHasForgetβ π Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.HasForgetβ (CategoryTheory.DifferentialObject S C) C - CategoryTheory.DifferentialObject.instHasShift π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.HasShift (CategoryTheory.DifferentialObject S C) S - CategoryTheory.DifferentialObject.hasZeroMorphisms π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] : CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.hasZeroObject π Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) [AddMonoidWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] : CategoryTheory.Limits.HasZeroObject (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.Hom.f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (self : X.Hom Y) : X.obj βΆ Y.obj - CategoryTheory.DifferentialObject.Hom.comp π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X.Hom Y) (g : Y.Hom Z) : X.Hom Z - CategoryTheory.DifferentialObject.isoApp π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X β Y) : X.obj β Y.obj - CategoryTheory.DifferentialObject.shiftFunctor π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (n : S) : CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.Hom.id_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : (CategoryTheory.DifferentialObject.Hom.id X).f = CategoryTheory.CategoryStruct.id X.obj - CategoryTheory.DifferentialObject.isoApp_refl π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : CategoryTheory.DifferentialObject.isoApp (CategoryTheory.Iso.refl X) = CategoryTheory.Iso.refl X.obj - CategoryTheory.DifferentialObject.d π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) : self.obj βΆ (CategoryTheory.shiftFunctor C 1).obj self.obj - CategoryTheory.DifferentialObject.instZeroHom π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] {X Y : CategoryTheory.DifferentialObject S C} : Zero (X βΆ Y) - CategoryTheory.DifferentialObject.id_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : (CategoryTheory.CategoryStruct.id X).f = CategoryTheory.CategoryStruct.id X.obj - CategoryTheory.DifferentialObject.Hom.ext π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} {instβ : AddMonoidWithOne S} {C : Type u} {instβΒΉ : CategoryTheory.Category.{v, u} C} {instβΒ² : CategoryTheory.Limits.HasZeroMorphisms C} {instβΒ³ : CategoryTheory.HasShift C S} {X Y : CategoryTheory.DifferentialObject S C} {x y : X.Hom Y} (f : x.f = y.f) : x = y - CategoryTheory.DifferentialObject.Hom.ext_iff π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} {instβ : AddMonoidWithOne S} {C : Type u} {instβΒΉ : CategoryTheory.Category.{v, u} C} {instβΒ² : CategoryTheory.Limits.HasZeroMorphisms C} {instβΒ³ : CategoryTheory.HasShift C S} {X Y : CategoryTheory.DifferentialObject S C} {x y : X.Hom Y} : x = y β x.f = y.f - CategoryTheory.DifferentialObject.isoApp_symm π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X β Y) : CategoryTheory.DifferentialObject.isoApp f.symm = (CategoryTheory.DifferentialObject.isoApp f).symm - CategoryTheory.DifferentialObject.isoApp_hom π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X β Y) : (CategoryTheory.DifferentialObject.isoApp f).hom = f.hom.f - CategoryTheory.DifferentialObject.isoApp_inv π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X β Y) : (CategoryTheory.DifferentialObject.isoApp f).inv = f.inv.f - CategoryTheory.DifferentialObject.eqToHom_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (h : X = Y) : (CategoryTheory.eqToHom h).f = CategoryTheory.eqToHom β― - CategoryTheory.DifferentialObject.Hom.comp_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X.Hom Y) (g : Y.Hom Z) : (f.comp g).f = CategoryTheory.CategoryStruct.comp f.f g.f - CategoryTheory.DifferentialObject.shiftZero π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.DifferentialObject.shiftFunctor C 0 β CategoryTheory.Functor.id (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.isoApp_trans π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X β Y) (g : Y β Z) : CategoryTheory.DifferentialObject.isoApp (f βͺβ« g) = CategoryTheory.DifferentialObject.isoApp f βͺβ« CategoryTheory.DifferentialObject.isoApp g - CategoryTheory.DifferentialObject.ext π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {A B : CategoryTheory.DifferentialObject S C} {f g : A βΆ B} (w : f.f = g.f := by aesop_cat) : f = g - CategoryTheory.DifferentialObject.ext_iff π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {A B : CategoryTheory.DifferentialObject S C} {f g : A βΆ B} : f = g β autoParam (f.f = g.f) _autoβ - CategoryTheory.DifferentialObject.comp_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X βΆ Y) (g : Y βΆ Z) : (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f - CategoryTheory.DifferentialObject.shiftFunctorAdd π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (m n : S) : CategoryTheory.DifferentialObject.shiftFunctor C (m + n) β (CategoryTheory.DifferentialObject.shiftFunctor C m).comp (CategoryTheory.DifferentialObject.shiftFunctor C n) - CategoryTheory.DifferentialObject.zero_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] (P Q : CategoryTheory.DifferentialObject S C) : CategoryTheory.DifferentialObject.Hom.f 0 = 0 - CategoryTheory.DifferentialObject.shiftFunctor_obj_obj π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctor C n).obj X).obj = (CategoryTheory.shiftFunctor C n).obj X.obj - CategoryTheory.DifferentialObject.Hom.comm π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (self : X.Hom Y) : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map self.f) = CategoryTheory.CategoryStruct.comp self.f Y.d - CategoryTheory.DifferentialObject.Hom.mk π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj βΆ Y.obj) (comm : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) = CategoryTheory.CategoryStruct.comp f Y.d := by aesop_cat) : X.Hom Y - CategoryTheory.Functor.mapDifferentialObject π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (D : Type u') [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (Ξ· : (CategoryTheory.shiftFunctor C 1).comp F βΆ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : β (c c' : C), F.map 0 = 0) : CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) (CategoryTheory.DifferentialObject S D) - CategoryTheory.DifferentialObject.mkIso π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj β Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d) : X β Y - CategoryTheory.DifferentialObject.Hom.comm_assoc π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (self : X.Hom Y) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj Y.obj βΆ Z) : CategoryTheory.CategoryStruct.comp X.d (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.f) h) = CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp Y.d h) - CategoryTheory.DifferentialObject.mkIso_hom_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj β Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d) : (CategoryTheory.DifferentialObject.mkIso f hf).hom.f = f.hom - CategoryTheory.DifferentialObject.mkIso_inv_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj β Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d) : (CategoryTheory.DifferentialObject.mkIso f hf).inv.f = f.inv - CategoryTheory.Functor.mapDifferentialObject_obj_obj π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (D : Type u') [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (Ξ· : (CategoryTheory.shiftFunctor C 1).comp F βΆ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : β (c c' : C), F.map 0 = 0) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.Functor.mapDifferentialObject D F Ξ· hF).obj X).obj = F.obj X.obj - CategoryTheory.DifferentialObject.mk π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (obj : C) (d : obj βΆ (CategoryTheory.shiftFunctor C 1).obj obj) (d_squared : CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0 := by aesop_cat) : CategoryTheory.DifferentialObject S C - CategoryTheory.DifferentialObject.d_squared π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) : CategoryTheory.CategoryStruct.comp self.d ((CategoryTheory.shiftFunctor C 1).map self.d) = 0 - CategoryTheory.DifferentialObject.Hom.mk.injEq π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj βΆ Y.obj) (comm : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) = CategoryTheory.CategoryStruct.comp f Y.d := by aesop_cat) (fβ : X.obj βΆ Y.obj) (commβ : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map fβ) = CategoryTheory.CategoryStruct.comp fβ Y.d := by aesop_cat) : ({ f := f, comm := comm } = { f := fβ, comm := commβ }) = (f = fβ) - CategoryTheory.DifferentialObject.d_squared_assoc π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj self.obj) βΆ Z) : CategoryTheory.CategoryStruct.comp self.d (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.d) h) = CategoryTheory.CategoryStruct.comp 0 h - CategoryTheory.Functor.mapDifferentialObject_obj_d π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (D : Type u') [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (Ξ· : (CategoryTheory.shiftFunctor C 1).comp F βΆ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : β (c c' : C), F.map 0 = 0) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.Functor.mapDifferentialObject D F Ξ· hF).obj X).d = CategoryTheory.CategoryStruct.comp (F.map X.d) (Ξ·.app X.obj) - CategoryTheory.DifferentialObject.shiftFunctor_obj_d π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctor C n).obj X).d = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map X.d) (CategoryTheory.shiftComm X.obj 1 n).hom - CategoryTheory.DifferentialObject.Hom.mk.sizeOf_spec π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} [SizeOf S] [SizeOf C] (f : X.obj βΆ Y.obj) (comm : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) = CategoryTheory.CategoryStruct.comp f Y.d := by aesop_cat) : sizeOf { f := f, comm := comm } = 1 + sizeOf f + sizeOf comm - CategoryTheory.DifferentialObject.shiftZero_hom_app_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftZero C).hom.app X).f = (CategoryTheory.shiftFunctorZero C S).hom.app X.obj - CategoryTheory.DifferentialObject.shiftZero_inv_app_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftZero C).inv.app X).f = (CategoryTheory.shiftFunctorZero C S).inv.app X.obj - CategoryTheory.DifferentialObject.mk.injEq π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (obj : C) (d : obj βΆ (CategoryTheory.shiftFunctor C 1).obj obj) (d_squared : CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0 := by aesop_cat) (objβ : C) (dβ : objβ βΆ (CategoryTheory.shiftFunctor C 1).obj objβ) (d_squaredβ : CategoryTheory.CategoryStruct.comp dβ ((CategoryTheory.shiftFunctor C 1).map dβ) = 0 := by aesop_cat) : ({ obj := obj, d := d, d_squared := d_squared } = { obj := objβ, d := dβ, d_squared := d_squaredβ }) = (obj = objβ β§ HEq d dβ) - CategoryTheory.DifferentialObject.shiftFunctorAdd_hom_app_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (m n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).hom.app X).f = (CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj - CategoryTheory.DifferentialObject.shiftFunctorAdd_inv_app_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (m n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).inv.app X).f = (CategoryTheory.shiftFunctorAdd C m n).inv.app X.obj - CategoryTheory.DifferentialObject.mk.sizeOf_spec π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [SizeOf S] [SizeOf C] (obj : C) (d : obj βΆ (CategoryTheory.shiftFunctor C 1).obj obj) (d_squared : CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0 := by aesop_cat) : sizeOf { obj := obj, d := d, d_squared := d_squared } = 1 + sizeOf obj + sizeOf d + sizeOf d_squared - CategoryTheory.DifferentialObject.shiftFunctor_map_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (n : S) {Xβ Yβ : CategoryTheory.DifferentialObject S C} (f : Xβ βΆ Yβ) : ((CategoryTheory.DifferentialObject.shiftFunctor C n).map f).f = (CategoryTheory.shiftFunctor C n).map f.f - CategoryTheory.Functor.mapDifferentialObject_map_f π Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (D : Type u') [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (Ξ· : (CategoryTheory.shiftFunctor C 1).comp F βΆ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : β (c c' : C), F.map 0 = 0) {Xβ Yβ : CategoryTheory.DifferentialObject S C} (f : Xβ βΆ Yβ) : ((CategoryTheory.Functor.mapDifferentialObject D F Ξ· hF).map f).f = F.map f.f - CategoryTheory.DifferentialObject.objEqToHom π Mathlib.Algebra.Homology.DifferentialObject
{Ξ² : Type u_1} [AddCommGroup Ξ²] {b : Ξ²} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject β€ (CategoryTheory.GradedObjectWithShift b V)) {i j : Ξ²} (h : i = j) : X.obj i βΆ X.obj j - CategoryTheory.DifferentialObject.objEqToHom_refl π Mathlib.Algebra.Homology.DifferentialObject
{Ξ² : Type u_1} [AddCommGroup Ξ²] {b : Ξ²} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject β€ (CategoryTheory.GradedObjectWithShift b V)) (i : Ξ²) : X.objEqToHom β― = CategoryTheory.CategoryStruct.id (X.obj i) - CategoryTheory.DifferentialObject.eqToHom_f' π Mathlib.Algebra.Homology.DifferentialObject
{Ξ² : Type u_1} [AddCommGroup Ξ²] {b : Ξ²} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : CategoryTheory.DifferentialObject β€ (CategoryTheory.GradedObjectWithShift b V)} (f : X βΆ Y) {x y : Ξ²} (h : x = y) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (f.f y) = CategoryTheory.CategoryStruct.comp (f.f x) (Y.objEqToHom h) - CategoryTheory.DifferentialObject.eqToHom_f'_assoc π Mathlib.Algebra.Homology.DifferentialObject
{Ξ² : Type u_1} [AddCommGroup Ξ²] {b : Ξ²} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : CategoryTheory.DifferentialObject β€ (CategoryTheory.GradedObjectWithShift b V)} (f : X βΆ Y) {x y : Ξ²} (h : x = y) {Z : V} (hβ : Y.obj y βΆ Z) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (CategoryTheory.CategoryStruct.comp (f.f y) hβ) = CategoryTheory.CategoryStruct.comp (f.f x) (CategoryTheory.CategoryStruct.comp (Y.objEqToHom h) hβ) - CategoryTheory.DifferentialObject.objEqToHom_d π Mathlib.Algebra.Homology.DifferentialObject
{Ξ² : Type u_1} [AddCommGroup Ξ²] {b : Ξ²} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject β€ (CategoryTheory.GradedObjectWithShift b V)) {x y : Ξ²} (h : x = y) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (X.d y) = CategoryTheory.CategoryStruct.comp (X.d x) (X.objEqToHom β―) - CategoryTheory.DifferentialObject.d_squared_apply π Mathlib.Algebra.Homology.DifferentialObject
{Ξ² : Type u_1} [AddCommGroup Ξ²] {b : Ξ²} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject β€ (CategoryTheory.GradedObjectWithShift b V)) {x : Ξ²} : CategoryTheory.CategoryStruct.comp (X.d x) (X.d ((fun b_1 => b_1 + { as := 1 }.as β’ b) x)) = 0 - CategoryTheory.DifferentialObject.objEqToHom_d_assoc π Mathlib.Algebra.Homology.DifferentialObject
{Ξ² : Type u_1} [AddCommGroup Ξ²] {b : Ξ²} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject β€ (CategoryTheory.GradedObjectWithShift b V)) {x y : Ξ²} (h : x = y) {Z : V} (hβ : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).obj X.obj y βΆ Z) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (CategoryTheory.CategoryStruct.comp (X.d y) hβ) = CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.objEqToHom β―) hβ) - CategoryTheory.DifferentialObject.d_squared_apply_assoc π Mathlib.Algebra.Homology.DifferentialObject
{Ξ² : Type u_1} [AddCommGroup Ξ²] {b : Ξ²} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject β€ (CategoryTheory.GradedObjectWithShift b V)) {x : Ξ²} {Z : V} (h : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).obj X.obj (x + 1 β’ b) βΆ Z) : CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.d (x + 1 β’ b)) h) = CategoryTheory.CategoryStruct.comp 0 h - instFreeMvPolynomialKaehlerDifferential π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] (Ο : Type u_1) : Module.Free (MvPolynomial Ο R) (Ξ©[MvPolynomial Ο RβR]) - KaehlerDifferential.mvPolynomialBasis π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] (Ο : Type u_1) : Basis Ο (MvPolynomial Ο R) (Ξ©[MvPolynomial Ο RβR]) - KaehlerDifferential.polynomialEquiv π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] : Ξ©[Polynomial RβR] ββ[Polynomial R] Polynomial R - KaehlerDifferential.mvPolynomialEquiv π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] (Ο : Type u_1) : Ξ©[MvPolynomial Ο RβR] ββ[MvPolynomial Ο R] Ο ββ MvPolynomial Ο R - KaehlerDifferential.mvPolynomialBasis_apply π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] (Ο : Type u_1) (i : Ο) : (KaehlerDifferential.mvPolynomialBasis R Ο) i = (KaehlerDifferential.D R (MvPolynomial Ο R)) (MvPolynomial.X i) - KaehlerDifferential.polynomialEquiv_D π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] (P : Polynomial R) : (KaehlerDifferential.polynomialEquiv R) ((KaehlerDifferential.D R (Polynomial R)) P) = Polynomial.derivative P - KaehlerDifferential.mvPolynomialBasis_repr_D_X π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] (Ο : Type u_1) (i : Ο) : (KaehlerDifferential.mvPolynomialBasis R Ο).repr ((KaehlerDifferential.D R (MvPolynomial Ο R)) (MvPolynomial.X i)) = funβ | i => 1 - KaehlerDifferential.mvPolynomialBasis_repr_apply π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] (Ο : Type u_1) (x : MvPolynomial Ο R) (i : Ο) : ((KaehlerDifferential.mvPolynomialBasis R Ο).repr ((KaehlerDifferential.D R (MvPolynomial Ο R)) x)) i = (MvPolynomial.pderiv i) x - KaehlerDifferential.polynomial_D_apply π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] (P : Polynomial R) : (KaehlerDifferential.D R (Polynomial R)) P = Polynomial.derivative P β’ (KaehlerDifferential.D R (Polynomial R)) Polynomial.X - KaehlerDifferential.polynomialEquiv_symm π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] (P : Polynomial R) : (KaehlerDifferential.polynomialEquiv R).symm P = P β’ (KaehlerDifferential.D R (Polynomial R)) Polynomial.X - KaehlerDifferential.mvPolynomialBasis_repr_D π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] (Ο : Type u_1) (x : MvPolynomial Ο R) : (KaehlerDifferential.mvPolynomialBasis R Ο).repr ((KaehlerDifferential.D R (MvPolynomial Ο R)) x) = (MvPolynomial.mkDerivation R fun x => funβ | x => 1) x - KaehlerDifferential.mvPolynomialBasis_repr_symm_single π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] (Ο : Type u_1) (i : Ο) (x : MvPolynomial Ο R) : ((KaehlerDifferential.mvPolynomialBasis R Ο).repr.symm funβ | i => x) = x β’ (KaehlerDifferential.D R (MvPolynomial Ο R)) (MvPolynomial.X i) - KaehlerDifferential.mvPolynomialBasis_repr_comp_D π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] (Ο : Type u_1) : (β(KaehlerDifferential.mvPolynomialBasis R Ο).repr).compDer (KaehlerDifferential.D R (MvPolynomial Ο R)) = MvPolynomial.mkDerivation R fun x => funβ | x => 1 - KaehlerDifferential.polynomialEquiv_comp_D π Mathlib.RingTheory.Kaehler.Polynomial
(R : Type u) [CommRing R] : (KaehlerDifferential.polynomialEquiv R).compDer (KaehlerDifferential.D R (Polynomial R)) = Polynomial.derivative' - Algebra.Presentation.differentialsRelations π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) : Module.Relations S - Algebra.Presentation.differentialsRelations_R π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) : pres.differentialsRelations.R = pres.rels - Algebra.Presentation.differentialsRelations_G π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) : pres.differentialsRelations.G = pres.vars - Algebra.Presentation.differentials π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) : Module.Presentation S (Ξ©[SβR]) - Algebra.Presentation.differentialsSolution π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) : pres.differentialsRelations.Solution (Ξ©[SβR]) - Algebra.Presentation.differentialsSolution_isPresentation π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) : pres.differentialsSolution.IsPresentation - Algebra.Presentation.differentials.homβ π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) : (pres.rels ββ S) ββ[S] pres.toExtension.Cotangent - Algebra.Presentation.differentials.surjective_homβ π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) : Function.Surjective β(Algebra.Presentation.differentials.homβ pres) - Algebra.Presentation.differentials.homβ.eq_1 π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) : Algebra.Presentation.differentials.homβ pres = Finsupp.linearCombination S fun r => Algebra.Extension.Cotangent.mk β¨pres.relation r, β―β© - Algebra.Presentation.differentialsRelations.eq_1 π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) : pres.differentialsRelations = { G := pres.vars, R := pres.rels, relation := fun r => Finsupp.mapRange β(algebraMap pres.Ring S) β― ((KaehlerDifferential.mvPolynomialBasis R pres.vars).repr ((KaehlerDifferential.D R (MvPolynomial pres.vars R)) (pres.relation r))) } - Algebra.Presentation.differentials.commββ π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) : pres.toExtension.toKaehler ββ βpres.cotangentSpaceBasis.repr.symm = pres.differentialsSolution.Ο - Algebra.Presentation.differentials.homβ_single π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) (r : pres.rels) : ((Algebra.Presentation.differentials.homβ pres) funβ | r => 1) = Algebra.Extension.Cotangent.mk β¨pres.relation r, β―β© - Algebra.Presentation.differentials.commββ' π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) : pres.toExtension.toKaehler ββ βpres.cotangentSpaceBasis.repr.symm = Finsupp.linearCombination S fun g => (KaehlerDifferential.D R S) (pres.val g) - Algebra.Presentation.differentials.commββ π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) : pres.toExtension.cotangentComplex ββ Algebra.Presentation.differentials.homβ pres = βpres.cotangentSpaceBasis.repr.symm ββ pres.differentialsRelations.map - Algebra.Presentation.differentials.commββ_single π Mathlib.Algebra.Module.Presentation.Differentials
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S) (r : pres.rels) : pres.toExtension.cotangentComplex ((Algebra.Presentation.differentials.homβ pres) funβ | r => 1) = pres.cotangentSpaceBasis.repr.symm (pres.differentialsRelations.relation r) - Algebra.PreSubmersivePresentation.differential π Mathlib.RingTheory.Smooth.StandardSmooth
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) : (P.rels β P.Ring) ββ[P.Ring] P.rels β P.Ring - Algebra.PreSubmersivePresentation.differential.eq_1 π Mathlib.RingTheory.Smooth.StandardSmooth
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) : P.differential = (P.basis.constr P.Ring) fun j i => (MvPolynomial.pderiv (P.map i)) (P.relation j) - CategoryTheory.SingleObj.differenceFunctor π Mathlib.CategoryTheory.SingleObj
{G : Type u} [Group G] {C : Type v} [CategoryTheory.Category.{w, v} C] (f : C β G) : CategoryTheory.Functor C (CategoryTheory.SingleObj G) - CategoryTheory.SingleObj.differenceFunctor_obj π Mathlib.CategoryTheory.SingleObj
{G : Type u} [Group G] {C : Type v} [CategoryTheory.Category.{w, v} C] (f : C β G) (xβ : C) : (CategoryTheory.SingleObj.differenceFunctor f).obj xβ = () - CategoryTheory.SingleObj.differenceFunctor_map π Mathlib.CategoryTheory.SingleObj
{G : Type u} [Group G] {C : Type v} [CategoryTheory.Category.{w, v} C] (f : C β G) {x y : C} (xβ : x βΆ y) : (CategoryTheory.SingleObj.differenceFunctor f).map xβ = f y * (f x)β»ΒΉ - differentiable_id π Mathlib.Analysis.Calculus.FDeriv.Basic
{π : Type u_1} [NontriviallyNormedField π] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π E] : Differentiable π id - differentiable_id' π Mathlib.Analysis.Calculus.FDeriv.Basic
{π : Type u_1} [NontriviallyNormedField π] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π E] : Differentiable π fun x => x - differentiableAt_id π Mathlib.Analysis.Calculus.FDeriv.Basic
{π : Type u_1} [NontriviallyNormedField π] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π E] {x : E} : DifferentiableAt π id x - differentiableAt_id' π Mathlib.Analysis.Calculus.FDeriv.Basic
{π : Type u_1} [NontriviallyNormedField π] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π E] {x : E} : DifferentiableAt π (fun x => x) x
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. 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:
By constant:
πReal.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
π"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.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
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 findtsum_lt_tsum
even though the hypothesisf i < g i
is not the last.
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, _ * _, _ ^ _, |- _ < _ β _
woould 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.
This is Loogle revision 026c9d9
serving mathlib revision a608095