Theorems · Theorem · group theory

Monoid.PushoutI.inf_of_range_eq_base_range

∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i},
  (∀ (i : ι), Function.Injective ⇑(φ i)) →
    ∀ {i j : ι}, i ≠ j → (Monoid.PushoutI.of i).range ⊓ (Monoid.PushoutI.of j).range = (Monoid.PushoutI.base φ).range

The intersection of the images of the maps from any two distinct groups in the diagram into the amalgamated product is the image of the map from the base group in the diagram.

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

0 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupGroup