Loogle!

Result

Found 19 declarations mentioning Algebra.PreSubmersivePresentation.map.

• Algebra.PreSubmersivePresentation.map 📋 Mathlib.RingTheory.Smooth.StandardSmooth
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (self : Algebra.PreSubmersivePresentation R S) : self.rels → self.vars
• Algebra.PreSubmersivePresentation.localizationAway_map 📋 Mathlib.RingTheory.Smooth.StandardSmooth
  {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] (x✝ : (Algebra.Presentation.localizationAway S r).rels) : (Algebra.PreSubmersivePresentation.localizationAway S r).map x✝ = ()
• Algebra.PreSubmersivePresentation.map_inj 📋 Mathlib.RingTheory.Smooth.StandardSmooth
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (self : Algebra.PreSubmersivePresentation R S) : Function.Injective self.map
• Algebra.PreSubmersivePresentation.baseChange.eq_1 📋 Mathlib.RingTheory.Smooth.StandardSmooth
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] (P : Algebra.PreSubmersivePresentation R S) : Algebra.PreSubmersivePresentation.baseChange T P = { toPresentation := Algebra.Presentation.baseChange T P.toPresentation, map := P.map, map_inj := ⋯, relations_finite := ⋯ }
• Algebra.PreSubmersivePresentation.comp_map 📋 Mathlib.RingTheory.Smooth.StandardSmooth
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.PreSubmersivePresentation S T) (P : Algebra.PreSubmersivePresentation R S) (a✝ : Q.rels ⊕ P.rels) : (Q.comp P).map a✝ = Sum.elim (fun rq => Sum.inl (Q.map rq)) (fun rp => Sum.inr (P.map rp)) a✝
• Algebra.PreSubmersivePresentation.reindex_map 📋 Mathlib.RingTheory.Smooth.StandardSmooth
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) {ι : Type u_1} {κ : Type u_2} (e : ι ≃ P.vars) (f : κ ≃ P.rels) (a✝ : (P.reindex e f).rels) : (P.reindex e f).map a✝ = (⇑e.symm ∘ P.map ∘ ⇑f) a✝
• Algebra.PreSubmersivePresentation.jacobiMatrix_apply 📋 Mathlib.RingTheory.Smooth.StandardSmooth
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) [Fintype P.rels] [DecidableEq P.rels] (i j : P.rels) : P.jacobiMatrix i j = (MvPolynomial.pderiv (P.map i)) (P.relation j)
• Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation 📋 Mathlib.RingTheory.Smooth.StandardSmooth
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.SubmersivePresentation R S) : LinearIndependent S fun i j => (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map j)) (P.relation i))
• Algebra.PreSubmersivePresentation.aevalDifferential_single 📋 Mathlib.RingTheory.Smooth.StandardSmooth
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) [DecidableEq P.rels] (i j : P.rels) : P.aevalDifferential (Pi.single i 1) j = (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map j)) (P.relation i))
• Algebra.SubmersivePresentation.basisDeriv_apply 📋 Mathlib.RingTheory.Smooth.StandardSmooth
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.SubmersivePresentation R S) (i j : P.rels) : P.basisDeriv i j = (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map j)) (P.relation i))
• 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)
• Algebra.SubmersivePresentation.basisKaehler 📋 Mathlib.RingTheory.Smooth.StandardSmoothCotangent
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.SubmersivePresentation R S) : Basis (↑(Set.range P.map)ᶜ) S (Ω[S⁄R])
• Algebra.SubmersivePresentation.basisKaehlerOfIsCompl 📋 Mathlib.RingTheory.Smooth.StandardSmoothCotangent
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.SubmersivePresentation R S) {κ : Type u_3} {f : κ → P.vars} (hf : Function.Injective f) (hcompl : IsCompl (Set.range f) (Set.range P.map)) : Basis κ S (Ω[S⁄R])
• Algebra.PreSubmersivePresentation.cotangentComplexAux.eq_1 📋 Mathlib.RingTheory.Smooth.StandardSmoothCotangent
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) : P.cotangentComplexAux = ↑(Finsupp.linearEquivFunOnFinite S S P.rels) ∘ₗ Finsupp.lcomapDomain P.map ⋯ ∘ₗ ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
• Algebra.PreSubmersivePresentation.cotangentComplexAux_apply 📋 Mathlib.RingTheory.Smooth.StandardSmoothCotangent
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) (x : ↥P.ker) (i : P.rels) : P.cotangentComplexAux (Algebra.Extension.Cotangent.mk x) i = (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map i)) ↑x)
• Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff 📋 Mathlib.RingTheory.Smooth.StandardSmoothCotangent
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.PreSubmersivePresentation R S} (x : ↥P.ker) : P.cotangentComplexAux (Algebra.Extension.Cotangent.mk x) = 0 ↔ ∀ (i : P.rels), (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map i)) ↑x) = 0
• Algebra.SubmersivePresentation.sectionCotangent_zero_of_not_mem_range 📋 Mathlib.RingTheory.Smooth.StandardSmoothCotangent
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.SubmersivePresentation R S) (i : P.vars) (hi : i ∉ Set.range P.map) : P.sectionCotangent (P.cotangentSpaceBasis i) = 0
• Algebra.SubmersivePresentation.sectionCotangent.eq_1 📋 Mathlib.RingTheory.Smooth.StandardSmoothCotangent
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.SubmersivePresentation R S) : P.sectionCotangent = ↑P.cotangentEquiv.symm ∘ₗ ↑(Finsupp.linearEquivFunOnFinite S S P.rels) ∘ₗ Finsupp.lcomapDomain P.map ⋯ ∘ₗ ↑P.cotangentSpaceBasis.repr
• Algebra.SubmersivePresentation.sectionCotangent_eq_iff 📋 Mathlib.RingTheory.Smooth.StandardSmoothCotangent
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.SubmersivePresentation R S) (x : P.toExtension.CotangentSpace) (y : P.toExtension.Cotangent) : P.sectionCotangent x = y ↔ ∀ (i : P.rels), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i

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:

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.

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.

This is Loogle revision 19971e9 serving mathlib revision bce1d65